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

Anupam Das and Isabel Oitavem. Preprint. 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. Preprint. 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 algebra and extensions

Anupam Das and Damien Pous. Preprint. HAL

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 …

On the logical complexity of cyclic arithmetic

Anupam Das. Preprint. 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 …

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 …

Alternating time bounds from variants of focussed proof systems

Anupam Das. Preprint. PDF

Intuitionistic logic and the polynomial hierarchy We conduct a complexity-theoretic study of focussed proof systems, relating the alternation of synchronous and asynchronous phases in a proof to an appropriate alternating time hierarchy, for instance the polynomial hierarchy. We propose a notion of ‘over-focussing’ that admits non-branching invertible rules during synchronous phases, due to the fact …

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. DOI arXiv PDF

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. 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 …