Herbrand Proofs and Expansion Proofs as Decomposed Proofs

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Article numberexaa052
JournalJournal of Logic and Computation
DOIs
Publication statusPublished - 24 Oct 2020

Cite this