## 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. 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.

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 |

## Keywords

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

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)