Projects per year
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 language | English |
---|---|
Article number | exaa052 |
Pages (from-to) | 1711–1742 |
Number of pages | 32 |
Journal | Journal of Logic and Computation |
Volume | 30 |
Issue number | 8 |
Early online date | 24 Oct 2020 |
DOIs | |
Publication status | Published - 31 Dec 2020 |
Fingerprint
Dive into the research topics of 'Herbrand Proofs and Expansion Proofs as Decomposed Proofs'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Efficient and Natural Proof Systems
Guglielmi, A. (PI), Bruscoli, P. (CoI) & McCusker, G. (CoI)
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council