On the Proof Complexity of Deep Inference

Paola Bruscoli 1 Alessio Guglielmi 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (2), pp.34
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00441211
Contributeur : Alessio Guglielmi <>
Soumis le : mardi 15 décembre 2009 - 10:41:32
Dernière modification le : mardi 13 mars 2018 - 14:24:05
Document(s) archivé(s) le : jeudi 17 juin 2010 - 20:24:07

Fichier

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

Identifiants

  • HAL Id : inria-00441211, version 1

Collections

Citation

Paola Bruscoli, Alessio Guglielmi. On the Proof Complexity of Deep Inference. ACM Transactions on Computational Logic, Association for Computing Machinery, 2009, 10 (2), pp.34. 〈inria-00441211〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

116