Skip to Main content Skip to Navigation
Journal articles

Extension without Cut

Lutz Straßburger 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

https://hal.inria.fr/hal-00759215
Contributor : Lutz Straßburger <>
Submitted on : Friday, November 30, 2012 - 11:37:07 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Friday, March 1, 2013 - 3:47:21 AM

File

psppp.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Lutz Straßburger. 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⟩

Share

Metrics

Record views

309

Files downloads

381