### 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 | Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings |

Editors | Anil Nerode, Sergei Artemov |

Publisher | Springer |

Pages | 289-308 |

Number of pages | 20 |

ISBN (Print) | 9783319720555 |

DOIs | |

Publication status | 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

- Deep inference
- Expansion proofs
- First-order logic
- Herbrand’s theorem
- Structural proof theory

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

*Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings*(pp. 289-308). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10703). Springer. https://doi.org/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

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

}

TY - GEN

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 - Deep inference

KW - Expansion proofs

KW - First-order logic

KW - Herbrand’s theorem

KW - Structural proof theory

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 - Logical Foundations of Computer Science - International Symposium, LFCS 2018, Proceedings

A2 - Nerode, Anil

A2 - Artemov, Sergei

PB - Springer

ER -