Researcher in proof theory, logic and complexity
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 …
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 …
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 …
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 …
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 …
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 …
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 …
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 …