On the Proof Complexity of Deep Inference

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.

• Type: Journal
• Year: 2007
• Where: CORR
• Authors: Paola Bruscoli, Alessio Guglielmi
• Keywords: Analytic Deepinference Proof, CORR 2007, Deep-inference Proof Systems, Education, Proof Systems