期刊
JOURNAL OF LOGIC AND COMPUTATION
卷 -, 期 -, 页码 -出版社
OXFORD UNIV PRESS
DOI: 10.1093/logcom/exad068
关键词
Cyclic proof; cut-elimination; inductive definition
This paper investigates the cut-elimination in cyclic proof systems, focusing on the case of first-order logic with inductive definitions. By providing a specific example, it demonstrates that the use of cut rule is not possible in the cyclic proof system.
A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with inductive definitions does not hold. This paper shows that the conjecture is correct by giving a sequent not provable without the cut rule but provable in the cyclic proof system.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据