论文标题
通过限制电感谓词的疾病，用于恢复环保系统中切割性能的研究
A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
论文作者
论文摘要
循环证明系统的框架为具有归纳定义的逻辑提供了合理的证明系统。它还为此类逻辑提供了有效的自动证明搜索程序，而没有找到归纳假设。最近的研究表明，Cut-leimination属性是证明理论中最基本的属性之一，用于几种逻辑的环状证明系统。这些结果表明，避免削减规则的幼稚证明搜索是不够的。 本文表明，即使我们将语言限制为一元素归纳谓词和一元功能，截止性属性仍然在简单的循环证明系统中失败，旨在阐明为什么切除率在周期性证明系统中失败了。本文的结果比第一位作者先前的结果更敏锐，该结果使用两个三元感应谓词和一个单一函数符号给出了反例，以显示一阶逻辑的循环证明系统中切除率的失败。
The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for such logics without finding induction hypotheses. Recent researches have shown that the cut-elimination property, one of the most fundamental properties in proof theory, of cyclic proof systems for several logics does not hold. These results suggest that a naive proof search, which avoids the Cut rule, is not enough. This paper shows that the cut-elimination property still fails in a simple cyclic proof system even if we restrict languages to unary inductive predicates and unary functions, aiming to clarify why the cut-elimination property fails in the cyclic proof systems. The result in this paper is a sharper one than that of the first authors' previous result, which gave a counterexample using two ternary inductive predicates and a unary function symbol to show the failure of the cut-elimination property in the cyclic proof system of the first-order logic.
