Towards an Analysis of Proofs in Arithmetic
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915330823028736 |
|---|---|
| author | Leitsch, Alexander Lolić, Anela Mahler, Stella |
| author_facet | Leitsch, Alexander Lolić, Anela Mahler, Stella |
| contents | Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata admit (schematic) cut-elimination and the construction of Herbrand systems. This work focuses on the expressivity of proof schemata. We show that proof schemata can simulate primitive recursive arithmetic. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_05837 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards an Analysis of Proofs in Arithmetic Leitsch, Alexander Lolić, Anela Mahler, Stella Logic in Computer Science Inductive proofs can be represented as proof schemata, i.e. as parameterized sequences of proofs defined in a primitive recursive way. Applications of proof schemata can be found in the area of automated proof analysis where the schemata admit (schematic) cut-elimination and the construction of Herbrand systems. This work focuses on the expressivity of proof schemata. We show that proof schemata can simulate primitive recursive arithmetic. The translation of proofs in arithmetic to proof schemata can be considered as a crucial step in the analysis of inductive proofs. |
| title | Towards an Analysis of Proofs in Arithmetic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.05837 |