CYDER, for "CYclic DErivations for Recursive operators", is my Marie Skłodowska Curie project, conducted at the at the ILLC, University of Amsterdam, under the supervision of Yde Venema and Bahareh Afshari. This project has received funding from the European Union under the HorizonEU research and innovation programme, Marie Skłodowska-Curie grant agreement No 101064105. Here you can find information about the project, its main research publications, and upcoming events and seminars related to CYDER's objectives.

Project information

• EC project: 101064105
• Call: MSCA-PF-2021
• Here you can find the project proposal, prepared using a LaTeX template
• Here you can find the evaluations of the proposal
• Duration of the project: September 2022 - August 2024

Main objectives
CYDER’s primary objective is to develop proof systems for modal fixpoint logics with frame conditions. These logics feature operators known as recursive modalities, which express notions defined recursively. Despite their wide-ranging applications in areas such as formal verification and knowledge representation, the proof theory for modal fixpoint logics remains relatively underexplored, with very few proof systems addressing logics with frame conditions.
To achieve this goal, CYDER will combine the formalism of labelled and structured proof systems, developed to define analytic and modular proof systems for families of modal logics with frame conditions, with cyclic proofs, which are analytic proof systems that co-inductively capture recursive modalities. By combining these approaches, the project aims to establish innovative proof methods for this challenging class of logics.

Future work
CYDER has made significant progress in meeting its objectives, with the introduction of novel methodologies in labelled and structured proof systems, as well as the definition of a (simple) proof system combining cyclic proofs and labelled calculi. However, a lot of work is still do be done, in particular in what concerns the definition of proof systesm for modal logics with recursive modalities and frame conditions. Stay tuned for more!

Publications

A simple loopcheck for intuitionistic K
joint work with Roman Kuznets, Sonia Marin, Marianela Morales and Lutz Straßburger
Proceedings of WoLLIC 2024 (doi, pdf)

Cyclic Hypersequent System for Transitive Closure Logic
joint work with Anupam Das
Journal of Automated Reasoning, 2023 (doi & pdf)

Intuitionistic S4 is decidable
joint work with Roman Kuznets, Sonia Marin, Marianela Morales and Lutz Straßburger
Proceedings of LICS 2023 (doi & pdf), extended version available here

Events
Workshop on Proof Systems for Modal Fixed Point Logics (29 and 30 January 2024, University of Amsterdam), webpage