Skip to Main content Skip to Navigation
Journal articles

Extension without Cut

Lutz Strassburger 1, 2 
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In proof theory one distinguishes sequent proofs with cut and cut-free sequent proofs, while for proof complexity one distinguishes Frege-systems and extended Frege-systems. In this paper we show how deep inference can provide a uniform treatment for both classifications, such that we can define cut-free systems with extension, which is neither possible with Frege-systems, nor with the sequent calculus. We show that the propositional pigeon-hole principle admits polynomial-size proofs in a cut-free system with extension. We also define cut-free systems with substitution and show that the cut-free system with extension p-simulates the cut-free system with substitution.
Document type :
Journal articles
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Friday, November 30, 2012 - 11:37:07 AM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Friday, March 1, 2013 - 3:47:21 AM


Files produced by the author(s)




Lutz Strassburger. Extension without Cut. Annals of Pure and Applied Logic, Elsevier Masson, 2012, 163 (12), pp.1995-2007. ⟨10.1016/j.apal.2012.07.004⟩. ⟨hal-00759215⟩



Record views


Files downloads