The project is about non-wellfounded and circular proof systems, particularly in the context of fixpoint logics. The standard approach in proof theory is to view a proof as a finite, wellfounded structure, in which the conclusion is justified step by step by a chain of inference steps that is eventually grounded in an axiom.

By contrast, non-wellfounded proof systems allow never-ending chains of inference steps, or cycles where the conclusion to be derived is assumed as a premise. Rather than being grounded in axioms, such inferences are considered valid or not depending on some global constraints on the structure of a proof. Non-wellfounded proof systems have turned out to be powerful tools for dealing with induktion and co-induction.

The aim of the project is to follow up on recent developments in this field, with the aim of developing complete proof systems for modal fixpoint logics, especially expressive extensions of the modal mu-calculus.