A Note on the Complexity of Classical and Intuitionistic Proofs

Matthias Baaz 1 Alexander Leitsch 1 Giselle Reis 2
1 TU WIEN - Technical University of Vienna [Vienna]
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 : —We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers (those without eigenvariable conditions): " There is an elementary function f such that if ϕ is a cut-free LK proof of A with symbol complexity ≤ c, then there exists a cut-free LJ proof of ¬¬A with symbol complexity ≤ f (c) ". This follows from the more general result: " There is an elementary function f such that if ϕ is a cut-free LK proof of A with symbol complexity ≤ c, then there exists a cut-free LJ proof of A with symbol complexity ≤ f (c) ". The result is proved using a suitable variant of cut-elimination by resolution (CERES) and subsumption.
Type de document :
Communication dans un congrès
LICS 2015 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2015, Kyoto, Japan. pp.657 - 666, 2015, 〈10.1109/LICS.2015.66〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01208346
Contributeur : Giselle Reis <>
Soumis le : vendredi 2 octobre 2015 - 14:20:02
Dernière modification le : dimanche 7 octobre 2018 - 01:09:21
Document(s) archivé(s) le : dimanche 3 janvier 2016 - 10:44:42

Fichier

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

Identifiants

Collections

INRIA | INSMI | UNIV-PARIS-SACLAY | LIX | X-LIX | X | X-DEP-INFO | PARISTECH

Citation

Matthias Baaz, Alexander Leitsch, Giselle Reis. A Note on the Complexity of Classical and Intuitionistic Proofs. LICS 2015 - 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2015, Kyoto, Japan. pp.657 - 666, 2015, 〈10.1109/LICS.2015.66〉. 〈hal-01208346〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

86

Contact


archive-ouverte@inria.fr