Projects per year
Abstract
The reduction of undecidable firstorder 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 firstorder logic, both with and without cut, such that ‘decomposed’ proofs—proofs where the contractive and noncontractive 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 (fromto)  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 
Projects
 1 Finished

Efficient and Natural Proof Systems
Guglielmi, A., Bruscoli, P. & McCusker, G.
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council