On the Proof Complexity of Deep Inference

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.

Minor improvements over the published version. Always updated version at <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>

References in corpus (5)

• A System of Interaction and Structure
• A System of Interaction and Structure II: The Need for Deep Inference
• Normalisation Control in Deep Inference via Atomic Flows
• Cirquent calculus deepened
• The three dimensions of proofs

Cited by in corpus (6)

• A System of Interaction and Structure IV: The Exponentials and Decomposition
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Subatomic Proof Systems: Splittable Systems
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• An Analytic Propositional Proof System on Graphs
• A Subatomic Proof System for Decision Trees