Extension without Cut - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Annals of Pure and Applied Logic Année : 2012

Extension without Cut

Résumé

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.
Fichier principal
Vignette du fichier
psppp.pdf (246.58 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00759215 , version 1 (30-11-2012)

Identifiants

Citer

Lutz Strassburger. Extension without Cut. Annals of Pure and Applied Logic, 2012, 163 (12), pp.1995-2007. ⟨10.1016/j.apal.2012.07.004⟩. ⟨hal-00759215⟩
121 Consultations
226 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More