CYDER · CYclic DErivations for Recursive operators

Modal fixpoint logics, which express recursive notions, find several fundamental applications in computer science. As a key example, in formal verification recursively defined notions are needed to reason about iterations of programs. A second prominent example comes from knowledge representation, where common knowledge of groups of agents is formalised through recursion. Much as in basic modal logics, the semantics of modal fixpoint logics can be enriched with additional properties, called frame conditions, to capture specific attitudes. Frame conditions give rise to rich and expressive families of modal fixpoint logics. Proof theory is the discipline that studies proof systems, which are sets of axioms and rules used to check validity of a formula. Proof systems play a central role in the analysis of logical systems. Despite their wide range of applications, the proof theory of modal fixpoint logics is currently underdeveloped. More specifically, the proof theory of modal fixpoint logics with frame conditions is much less advanced than the proof theory of modal or intuitionistic logics. The key objective of CYDER is to define proof systems for modal fixpoint logics with frame conditions, providing a general proof-theoretical framework for these logics. Towards this challenging aim, CYDER will define two new kinds of proof systems: labelled and nested cyclic proofs. CYDER proof-theoretical methodology is inspired by labelled and nested sequents, which capture modal logics with frame conditions, and cyclic proofs, which are a powerful formalism to treat recursion. The project will define cyclic proof systems for several systems of modal fixpoint logics: epistemic logics with common knowledge, the alternation-free modal mu-calculus with frame conditions, intuitionistic modal logics with recursive modalities and dynamic epistemic logics.