On the Proof Complexity of Deep Inference

Authors:
  • PBPaola Bruscoli
    Paola Bruscoli
  • AGAlessio Guglielmi
    Alessio Guglielmi

Abstract
We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, including when extended with the Tseitin extension rule and 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.