Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2402.13905 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929307079671808 |
|---|---|
| author | Leitsch, Alexander Lolic, Anela |
| author_facet | Leitsch, Alexander Lolic, Anela |
| contents | An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to analyze these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand's theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. We develop a new framework for schematic substitutions and define a unification algorithm for resolution schemata. Moreover, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand schema, which represents its Herbrand sequent. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_13905 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Herbrand's Theorem in Refutation Schemata Leitsch, Alexander Lolic, Anela Logic An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to analyze these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand's theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. We develop a new framework for schematic substitutions and define a unification algorithm for resolution schemata. Moreover, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand schema, which represents its Herbrand sequent. |
| title | Herbrand's Theorem in Refutation Schemata |
| topic | Logic |
| url | https://arxiv.org/abs/2402.13905 |