Unravelling Abstract Cyclic Proofs into Proofs by Induction
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911443326074880 |
|---|---|
| author | Grotenhuis, Lide Otten, Daniël |
| author_facet | Grotenhuis, Lide Otten, Daniël |
| contents | Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract cyclic proof systems with a well-founded induction principle, and transform any cyclic proof into a finite proof in the extended system. Moreover, this transformation preserves the structure of the cyclic proof.
Our results leverage an annotated representation of cyclic proofs, which allows us to extract induction hypotheses and to determine their introduction order. The representation is essentially a reset proof with one key modification: names must be covered in a uniform way before a reset. This innovation allows us to handle cyclic proofs where the underlying inductive sort is non-linear.
Our framework is general enough to cover recursive functions satisfying the size-change termination principle, which are viewed as cyclic proofs under the Curry-Howard correspondence. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_12054 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Unravelling Abstract Cyclic Proofs into Proofs by Induction Grotenhuis, Lide Otten, Daniël Logic in Computer Science Logic 03F07, 03F55 F.4.1; I.2.2; I.2.3 Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cyclic proofs with traditional finite proofs: we extend abstract cyclic proof systems with a well-founded induction principle, and transform any cyclic proof into a finite proof in the extended system. Moreover, this transformation preserves the structure of the cyclic proof. Our results leverage an annotated representation of cyclic proofs, which allows us to extract induction hypotheses and to determine their introduction order. The representation is essentially a reset proof with one key modification: names must be covered in a uniform way before a reset. This innovation allows us to handle cyclic proofs where the underlying inductive sort is non-linear. Our framework is general enough to cover recursive functions satisfying the size-change termination principle, which are viewed as cyclic proofs under the Curry-Howard correspondence. |
| title | Unravelling Abstract Cyclic Proofs into Proofs by Induction |
| topic | Logic in Computer Science Logic 03F07, 03F55 F.4.1; I.2.2; I.2.3 |
| url | https://arxiv.org/abs/2602.12054 |