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
Pages (from-to)1711–1742
Number of pages32
JournalJournal of Logic and Computation
Volume30
Issue number8
Early online date24 Oct 2020
DOIs
Publication statusPublished - 31 Dec 2020

Cite this