On the Proof Complexity of Deep Inference
Computational Complexity
2009-04-19 v3 Logic in Computer Science
Logic
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 speed-up over analytic Gentzen proof systems that they polynomially simulate.
Cite
@article{arxiv.0709.1201,
title = {On the Proof Complexity of Deep Inference},
author = {Paola Bruscoli and Alessio Guglielmi},
journal= {arXiv preprint arXiv:0709.1201},
year = {2009}
}
Comments
Minor improvements over the published version. Always updated version at <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>