HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Cited literature [39 references]  Display  Hide  Download

https://hal.inria.fr/inria-00441211
Contributor : Alessio Guglielmi Connect in order to contact the contributor
Submitted on : Tuesday, December 15, 2009 - 10:41:32 AM
Last modification on : Friday, February 4, 2022 - 3:12:22 AM
Long-term archiving on: : Thursday, June 17, 2010 - 8:24:07 PM

File

OnPrComplDI.pdf
Files produced by the author(s)

Identifiers

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. ⟨10.1145/1462179.1462186⟩. ⟨inria-00441211⟩

Share

Metrics

Record views

81

Files downloads

118