From QBFs to MALL and back via focussing

Anupam Das. Submitted. (Extended version of IJCAR '18 paper). arXiv

In this work we investigate how to extract alternating time bounds from ‘focussed’ proof systems. Our main result is the obtention of fragments of MALLw (MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show …

A Functional (Monadic) Second-Order Theory of Infinite Trees

Anupam Das and Colin Riba. Submitted. (Extended version of LICS '15 paper). arXiv

This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability (“Rabin’s Tree Theorem”) is one of the most powerful known results concerning the decidability of logics. By a complete axiomatization we mean a complete deduction system with a polynomial-time recognizable …

On the logical complexity of cyclic arithmetic

Anupam Das. Accepted to Logical Methods in Computer Science. arXiv PDF

We study the logical complexity of proofs in cyclic arithmetic , as introduced by Simpson, in terms of quantifier alternations of formulae occurring. Writing for (the logical consequences of) cyclic proofs containing only formulae, our main result is that and prove the same theorems, for . Furthermore, due to the ‘uniformity’ of our method, we …

Left-Handed Completeness for Kleene algebra, via Cyclic Proofs

Anupam Das, Amina Doumane and Damien Pous. In proceedings of LPAR '18. DOI HAL

We give a new proof that the axioms of left-handed Kleene algebra are complete with respect to language containments. This proof is significantly simpler than both the proof of Boffa (which relies on Krob’s completeness result), and the more recent proof of Kozen and Silva. Our proof builds on a recent non-wellfounded sequent calculus which …

A recursion-theoretic characterisation of the positive polynomial-time functions

Anupam Das and Isabel Oitavem. In proceedings of CSL '18. (Invited to special issue). DOI PDF

We extend work of Lautemann, Schwentick and Stewart on characterisations of the ‘positive’ polynomial-time predicates (posP, also called mP by Grigni and Sipser) to function classes. Our main result is the obtention of a function algebra for the positive polynomial-time functions (posFP), by imposing a simple uniformity condition on the bounded recursion operator in Cobham’s …

Focussing, MALL and the polynomial hierarchy

Anupam Das. In proceedings of IJCAR '18. (Invited to special issue). DOI PDF

We investigate how to extract alternating time bounds from ‘focussed’ proofs, treating non-invertible rule phases as nondeterministic computation and invertible rule phases as co-nondeterministic computation. We refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch, more faithfully associating phases of focussed …

Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)

Anupam Das and Damien Pous. In proceedings of CSL '18. DOI HAL PDF

We prove cut-elimination for a sequent-style proof system which is sound and complete for the equational theory of Kleene algebra, and where proofs are potentially non-wellfounded infinite trees. We extend these results to systems with meets and residuals, capturing ‘star-continuous’ action lattices in a similar way. We recover the equational theory of all action lattices …

A cut-free cyclic proof system for Kleene algebra

Anupam Das and Damien Pous. In proceedings of Tableaux '17. DOI HAL PDF

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 …