The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
From MaRDI portal
Publication:6504553
DOI10.1093/LOGCOM/EXAD068arXiv2106.11798MaRDI QIDQ6504553FDOQ6504553
Authors: Yukihiro Oda, James Brotherston, Makoto Tatsuta 
Abstract: 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.
This page was built for publication: The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6504553)
