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

https://hal.inria.fr/inria-00441211
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

File

OnPrComplDI.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

194

Files downloads

213