English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The framework of cyclic proof systems provides a reasonable proof system forlogics with inductive definitions. It also offers an effective automated proofsearch procedure for such logics without finding induction hypotheses. Recentresearches have shown that the cut-elimination property, one of the mostfundamental properties in proof theory, of cyclic proof systems for severallogics does not hold. These results suggest that a naive proof search, whichavoids the Cut rule, is not enough.  This paper shows that the cut-elimination property still fails in a simplecyclic proof system even if we restrict languages to unary inductive predicatesand unary functions, aiming to clarify why the cut-elimination property failsin the cyclic proof systems. The result in this paper is a sharper one thanthat of the first authors' previous result, which gave a counterexample usingtwo ternary inductive predicates and a unary function symbol to show thefailure of the cut-elimination property in the cyclic proof system of thefirst-order logic.

A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates