ABSTRACT. Cyclic and ill-founded proofs are an important alternative to proofs by induction. In cyclic proofs infinite paths are permitted as long as they follow the unfolding pattern characterising the validity of the inductive formulæ involved. It has been shown recently that, over modal logic, cyclic proofs coincide with proofs by explicit induction. This result was used to establish sound and complete cut-free axiomatisations for the modal mu-calculus, an extension of propositional modal logic which captures the essence of inductive and co-inductive reasoning. In this talk we will discuss the approach via cyclic modal proofs and their virtues as a proof system on their own right.

ABSTRACT. We propose LMSO, a proof system inspired from Linear Logic, as a proof-theoretical framework to extract finite-state stream transducers from linear-constructive proofs of omega-regular specifications. We advocate LMSO as a stepping stone toward semi-automatic approaches to Church’s synthesis com- bining computer assisted proofs with automatic decisions procedures. LMSO is correct in the sense that it comes with an automata-based realizability model in which proofs are interpreted as finite-state stream transducers. It is moreover complete, in the sense that every solvable instance of Church’s synthesis problem leads to a linear-constructive proof of the formula specifying the synthesis problem.

ABSTRACT. We propose a coinductive extension of Miller et. al.'s framework of uniform proof as a machinery for formulating and proving coinductive invariants arising from first-order Horn clause logic programming. It helps the study of coinductive logic programming.

ABSTRACT. Cyclic proofs have recently been gaining in popularity, both as a proof-theoretic tool for studying logical systems, and as a paradigm for automatic proof search.  Over two hour-long talks at the PARIS workshop I hope to give an introduction to cyclic proofs for the uninitiated, to explore some of their applications, to outline their relationships to other techniques and, perhaps, to clear up some common misconceptions.

ABSTRACT. Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. We present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria.

ABSTRACT. We study the logical complexity of proofs in cyclic arithmetic (CA), as introduced in Simpson '17, in terms of quantifier alternations of formulae occurring. Writing CΣ_n for (the logical consequences of) cyclic proofs containing only Σ_n formulae, our main result is that IΣ_{n+1} and CΣ_n prove the same Π_{n+1} theorems, for n > 0. Furthermore, due to the 'uniformity' of our method, we also show that CA and PA proofs differ only elementarily in size.

The inclusion IΣ_{n+1} ⊆ CΣ_n is obtained by proof theoretic techniques, relying on normal forms and structural manipulations of Peano arithmetic (PA) proofs. It improves upon the natural result that IΣ_n ⊆ CΣ_n.

The inclusion CΣ_n ⊆ IΣ_{n+1} is obtained by calibrating the approach of Simpson '17 with recent results on the reverse mathematics of Büchi’s theorem (Kolodziejczyk, Michalewski, Pradic & Skrzypczak '16), and specialising to the case of cyclic proofs.

These results improve upon the bounds on proof complexity and logical complexity implicit in Simpson '17 and Berardi & Tatsuta '17.

This talk will be based on the following work: http://www.anupamdas.com/wp/log-comp-cyc-arith/