Anupam Das (University of Birmingham, U.K.)

Cyclic proofs, a primer

Abstract: 'Cyclic' and 'non-wellfounded' proofs have emerged in the last 30 years as a powerful mechanism to reason about systems with (co)induction. They are an alternative to usual well-founded proofs with (co)induction principles, that are seemingly more powerful at the level of expressivity, and more intuitive at the level of proof search, often avoiding elusive invariants.
In this course we shall introduce students to the foundations of cyclic proof systems. We shall present the core theory, based on seminal results in the literature. Moreover we shall give the students the tools they need to apply these techniques to new logics and theories.