On circular reasoning and proof theory

Anupam Das

Anupam Das (Copenhagen) will present "On circular reasoning and proof theory" give at 11 on Thursday 20 December in Old Quad G10.

Abstract: Incorporating *circular reasoning* into proofs has become an increasingly useful tool in computational logic in the last 20 years. The idea is that replacing inductive invariants with a richer proof structure often enables us to more naturally reason about inductive structures, especially for logics arising from relational semantics. Moreover, much recent empirical evidence in verification suggests that proofs of termination or safety properties are more readily found in a cyclic system than an inductive one. Naturally some sort of external criterion must be imposed in order to avoid fallacious reasoning, and such criteria constitute an emerging bridge between proof theory and automata over infinite sets.

In this talk I will give a few examples of circular reasoning in action and, in particular, demonstrate the improved succinctness of Cyclic Proofs formally in the setting of arithmetic: cyclic proofs can prove the same theorems as inductive proofs, but with logically simpler formulae occurring in proofs. The result given is tight, in terms of the arithmetical hierarchy, and the two directions of the result require different sets of tools from structural proof theory, automaton theory and reverse mathematics. 

This talk will be partially based on the following preprint: https://arxiv.org/abs/1807.10248.