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 Inria Saclay - Ile de France
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
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 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 : samedi 18 février 2017 - 01:14:40
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

Citation

Matthias Baaz, Alexander Leitsch, Giselle Reis. A Note on the Complexity of Classical and Intuitionistic Proofs. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 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

227

Téléchargements de fichiers

85

Contact


archive-ouverte@inria.fr