Oda, Yukihiro;
Brotherston, James;
Tatsuta, Makoto;
(2023)
The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions.
Journal of Logic and Computation
, Article exad068. 10.1093/logcom/exad068.
(In press).
Preview |
Text
oda_brotherston_tatsuta_JLC24.pdf - Other Download (299kB) | Preview |
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.
| Type: | Article |
|---|---|
| Title: | The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1093/logcom/exad068 |
| Publisher version: | https://doi.org/10.1093/logcom/exad068 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10188190 |
Archive Staff Only
 |
View Item |
