On the Proof Complexity of Deep Inference
Paola Bruscoli, Alessio Guglielmi, Bath Ba Ay · The University of Bath Online Publications Store (The University of Bath) · 2000
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 deepinference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate. 1.