### Abstract

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. The problem of building a natural

proof system around expansion proofs, with composition of proofs

and cut-free completeness, has been approached from a variety of different

angles. In this paper we construct a simple deep inference system

for first-order logic, KSh2, based around the notion of expansion proofs,

as a starting point to developing a rich proof theory around this foundation.

Translations between proofs in this system and expansion proofs

are given, retaining much of the structure in each direction.

Original language | English |
---|---|

Title of host publication | Symposium on Logical Foundations in Computer Science 2018 |

Editors | Sergei Artemov, Anil Nerode |

Publisher | Springer |

Pages | 289-308 |

Number of pages | 20 |

ISBN (Print) | 9783319720555 |

DOIs | |

State | Published - 2018 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 10703 |

### Fingerprint

### Keywords

- proof theory
- deep inference
- expansion proofs
- structural proof theory
- Herbrand's theorem

### Cite this

*Symposium on Logical Foundations in Computer Science 2018*(pp. 289-308). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10703). Springer. DOI: 10.1007/978-3-319-72056-2_18

**A Natural Proof System for Herbrand's Theorem.** / Ralph, Benjamin.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Symposium on Logical Foundations in Computer Science 2018.*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10703, Springer, pp. 289-308. DOI: 10.1007/978-3-319-72056-2_18

}

TY - CHAP

T1 - A Natural Proof System for Herbrand's Theorem

AU - Ralph,Benjamin

PY - 2018

Y1 - 2018

N2 - The reduction of undecidable first-order logic to decidablepropositional logic via Herbrand’s theorem has long been of interest totheoretical computer science, with the notion of a Herbrand proof motivatingthe definition of expansion proofs. The problem of building a naturalproof system around expansion proofs, with composition of proofsand cut-free completeness, has been approached from a variety of differentangles. In this paper we construct a simple deep inference systemfor first-order logic, KSh2, based around the notion of expansion proofs,as a starting point to developing a rich proof theory around this foundation.Translations between proofs in this system and expansion proofsare given, retaining much of the structure in each direction.

AB - The reduction of undecidable first-order logic to decidablepropositional logic via Herbrand’s theorem has long been of interest totheoretical computer science, with the notion of a Herbrand proof motivatingthe definition of expansion proofs. The problem of building a naturalproof system around expansion proofs, with composition of proofsand cut-free completeness, has been approached from a variety of differentangles. In this paper we construct a simple deep inference systemfor first-order logic, KSh2, based around the notion of expansion proofs,as a starting point to developing a rich proof theory around this foundation.Translations between proofs in this system and expansion proofsare given, retaining much of the structure in each direction.

KW - proof theory

KW - deep inference

KW - expansion proofs

KW - structural proof theory

KW - Herbrand's theorem

U2 - 10.1007/978-3-319-72056-2_18

DO - 10.1007/978-3-319-72056-2_18

M3 - Conference contribution

SN - 9783319720555

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 289

EP - 308

BT - Symposium on Logical Foundations in Computer Science 2018

PB - Springer

ER -