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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Article dans une revue
Ann. Pure Appl. Logic, Elsevier, 2012, 163 (12), pp.1995-2007. 〈10.1016/j.apal.2012.07.004〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00759215
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 30 novembre 2012 - 11:37:07
Dernière modification le : jeudi 10 mai 2018 - 02:06:32
Document(s) archivé(s) le : vendredi 1 mars 2013 - 03:47:21

Fichier

psppp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lutz Straßburger. Extension without Cut. Ann. Pure Appl. Logic, Elsevier, 2012, 163 (12), pp.1995-2007. 〈10.1016/j.apal.2012.07.004〉. 〈hal-00759215〉

Partager

Métriques

Consultations de la notice

215

Téléchargements de fichiers

192