Loading...
Please wait, while we are loading the content...
Similar Documents
Herbrand Proofs and Expansion Proofs as Decomposed Proofs
| Content Provider | Oxford Academic |
|---|---|
| Author | Ralph, Benjamin |
| Copyright Year | 2020 |
| Abstract | The reduction of undecidable first-order logic to decidable propositional logic via Herbrand's theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. In this paper we construct simple deep inference systems for first-order logic, both with and without cut, such that 'decomposed' proofs—proofs where the contractive and non-contractive behaviour of the proof is separated—in each system correspond to either expansion proofs or Herbrand proofs. Translations between proofs in this system, expansion proofs and Herbrand proofs are given, retaining much of the structure in each direction. |
| Related Links | https://academic.oup.com/logcom/article-pdf/30/8/1711/34673322/exaa052.pdf |
| Ending Page | 1742 |
| Starting Page | 1711 |
| File Format | |
| ISSN | 0955792X |
| e-ISSN | 1465363X |
| DOI | 10.1093/logcom/exaa052 |
| Journal | Journal of Logic and Computation |
| Issue Number | 8 |
| Volume Number | 30 |
| Language | English |
| Publisher | Oxford Academic |
| Publisher Date | 2020-12-10 |
| Access Restriction | Open |
| Subject Keyword | Computer Architecture and Logic Design Computer Science Science and Mathematics |
| Content Type | Text |
| Resource Type | Article |
| Subject | Logic Theoretical Computer Science Hardware and Architecture Software |
