The complexity of propositional proofs in deep inference


Deep inference is a relatively recent proof methodology whose systems differ from traditional systems by allowing inference rules to operate on any connective appearing in a formula, rather than just the main connective. Its distinguishing feature, from a structural proof theoretic point of view, is that its systems are local : inference steps can be checked in constant time, a property impossible to achieve in Gentzen sequent calculi.

Due to the greater flexibility in applying inference rules, deep inference systems introduce more normal forms to classical proof theory, splitting Gentzen cut-elimination into smaller steps. While the complexity of full cut-elimination in the sequent calculus is necessarily exponential in the size of the input proof, these intermediate procedures exhibit varying complexities, while still entailing properties of proof theoretic interest, such as consistency and decidability.

This dissertation contributes to the classification of these intermediate classes of proof, from the point of view of proof complexity, and introduces new techniques to analyse their complexity.