Logic and complexity

Free-cut elimination in linear logic and an application to a feasible arithmetic

Patrick Baillot and Anupam Das. In proceedings of CSL '16. DOI HAL PDF

We prove a general form of ‘free-cut elimination’ for first-order theories in linear logic, yielding normal forms of proofs where cuts are anchored to nonlogical steps. To demonstrate the usefulness of this result, we consider a version of arithmetic in linear logic, based on a previous axiomatisation by Bellantoni and Hofmann. We prove a witnessing …

From positive and intuitionistic bounded arithmetic to monotone proof complexity

Anupam Das. In proceedings of LICS '16. DOI PDF

We study versions of second-order bounded arithmetic where induction and comprehension formulae are positive or where the underlying logic is intuitionistic, examining their relationships to monotone and deep inference proof systems for propositional logic. In the positive setting a restriction of a Paris-Wilkie (PW) style translation yields quasipolynomial-size monotone propositional proofs from Π01 arithmetic theorems, …

On the relative proof complexity of deep inference via atomic flows

Anupam Das. Logical Methods in Computer Science. Special issue of selected papers of the Turing Centenary Conference: CiE 2012. DOI arXiv PDF

We consider the proof complexity of the minimal complete fragment, KS, of standard deep inference systems for propositional logic. To examine the size of proofs we employ atomic flows, diagrams that trace structural changes through a proof but ignore logical information. As results we obtain a polynomial simulation of versions of Resolution, along with some …

On the pigeonhole and related principles in deep inference and monotone systems

Anupam Das. In proceedings of CSL-LICS '14. DOI PDF

We construct quasipolynomial-size proofs of the propositional pigeonhole principle in the deep inference system KS, addressing an open problem raised in previous works and matching the best known upper bound for the more general class of monotone proofs. We make significant use of monotone formulae computing boolean threshold functions, an idea previously considered in works …

The complexity of propositional proofs in deep inference

Anupam Das. PhD thesis. Supervised by Alessio Guglielmi and John Power, University of Bath. PDF

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 …

Complexity of deep inference via atomic flows

Anupam Das. In proceedings of Turing Centenary Conference: CiE 2012. DOI PDF

We consider the fragment of deep inference free of compression mechanisms and compare its proof complexity to other systems, utilising ‘atomic flows’ to examine size of proofs. Results include a simulation of Resolution and dag-like cut-free Gentzen, as well as a separation from bounded-depth Frege. NB: There are errors in some statements and proofs of …

Characterising aspects of proof compression

Anupam Das. Note. PDF

We consider deep inference proof formalisms, which are flexible enough to embed many widely used proof systems, and construe compression mechanisms `cut’ and `dag’ in a way that is independent of any particular proof system, but in a way that nonetheless has the same effect from the point of view of proof complexity. The main …

On the proof complexity of cut-free bounded deep inference

Anupam Das. In proceedings of Tableaux '11. DOI PDF

It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the …