Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [39 references]  Display  Hide  Download
Contributor : Alessio Guglielmi <>
Submitted on : Tuesday, December 15, 2009 - 10:41:32 AM
Last modification on : Tuesday, March 13, 2018 - 2:24:05 PM
Long-term archiving on: : Thursday, June 17, 2010 - 8:24:07 PM


Files produced by the author(s)


  • HAL Id : inria-00441211, version 1



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⟩



Record views


Files downloads