Proof complexity of deep inference: a survey

Author: Anupam Das

Paper Information

Title:Proof complexity of deep inference: a survey
Authors:Anupam Das
Proceedings:TYDI-0 Abstracts
Editor: Lutz Stra├čburger
Keywords:Proof complexity, Bounded arithmetic, Deep inference, Atomic flows, Contraction

ABSTRACT. In this talk I will survey the current state of research on the complexity of deep inference proofs in classical propositional logic, and also introduce a recent program of research to further develop this subject. Deep inference calculi, due to Guglielmi and others, differ from traditional systems by allowing proof rules to operate on *any* connective occurring in a formula, as opposed to just the main connective. Consequently such calculi are more fine-grained and admit smaller proofs of benchmark classes of tautologies. As well as plainly theoretical motivations, this is advantageous from the point of view of proof communication, allowing for compact and easy-to-check certificates for proofs. I present a graph-based formalism called 'atomic flows', due to Guglielmi and Gundersen following from previous work by Buss, and a rewriting system on them that models proof normalisation while preserving complexity properties. I show how such an abstraction has been influential in work up to now, allowing the obtention of surprisingly strong upper bounds and simulations in analytic deep inference. The biggest open question in the area is the relative complexity between the minimal system KS and a version that allows a form of sharing, KS+. To this end I will consider systems of bounded arithmetic to serve as uniform counterparts to these nonuniform propositional systems. Due to the peculiarities of deep inference calculi, the search for corresponding arithmetic theories takes us into the largely unexplored territories of intuitionistic and substructural arithmetics, requiring novel interplays of tools at the interface of logic and complexity.

Talk:Jul 07 17:00 (Session 31R: Contraction)