A cut-free cyclic proof system for Kleene algebra

Anupam Das and Damien Pous. Proceedings of Tableaux '17. DOIHALPreprintBIB
We introduce a sound non-wellfounded proof system whose regular (or ‘cyclic’) proofs are complete for (in)equations between regular expressions. We achieve regularity by using hypersequents rather than usual sequents, with more structure in the succedent, and relying on the discreteness of rational languages to drive proof search. By inspection of the proof search space we …

On linear rewriting systems for Boolean logic and some applications to proof theory

Anupam Das and Lutz Straßburger. Logical Methods in Computer Science. Special issue of selected papers from RTA and TLCA '15. DOIarXivPreprintBIB
Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In this paper we study properties of …

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

Patrick Baillot and Anupam Das. Proceedings of CSL '16. DOIHALPreprintBIB
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. Proceedings of LICS '16. DOIPreprintBIB
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 nested sequents for constructive modal logics

Ryuta Arisaka, Anupam Das and Lutz Straßburger. Logical Methods in Computer Science. DOIarXivPreprintBIB
We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism …

A complete axiomatization of MSO on infinite trees

Anupam Das and Colin Riba. Proceedings of LICS '15. DOIPreprintBIB
We show that an adaptation of Peano’s axioms for second-order arithmetic to the language of MSO completely axiomatizes the theory over infinite trees. This continues a line of work begun by Büchi and Siefkes with axiomatizations of MSO over various classes of linear orders. Our proof formalizes, in the axiomatic theory, a translation of MSO …

No complete linear term rewriting system for propositional logic

Anupam Das and Lutz Straßburger. Proceedings of RTA '15. DOIPreprintBIB
Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-) linear rewrite rule. This raises the question of whether there is a rewriting system on linear terms of propositional logic that is …

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. DOIarXivPreprintBIB
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. Proceedings of CSL-LICS '14. DOIPreprintBIB
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 …

Rewriting with linear inferences in propositional logic

Anupam Das. Proceedings of RTA '13. DOIPreprintBIB
Linear inferences are sound implications of propositional logic where each variable appears exactly once in the premiss and conclusion. We consider a specific set of these inferences, MS, first studied by Straßburger, corresponding to the logical rules in deep inference proof theory. Despite previous results characterising the individual rules of MS, we show that there …

Complexity of deep inference via atomic flows

Anupam Das. Proceedings of Turing Centenary Conference: CiE 2012. DOIPreprintBIB
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 …

On the proof complexity of cut-free bounded deep inference

Anupam Das. Proceedings of Tableaux '11. DOIPreprintBIB
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 …