Workshop on proof systems for modal fixed point logics

Workshop on Proof Systems for Modal Fixed Point Logics

On 29 and 30 January 2024 the workshop Proof Systems for Modal Fixed Point Logics takes place at the University of Amsterdam. The workshop is associated with two public PhD Defences. Guillermo Menéndez Turata will defend his thesis Cyclic Proof Systems for Modal Fixpoint Logics on 30 January at 13:00 in the Agnietenkapel. Jan Rooduijn will defend his thesis Fragments and Frame Classes: Towards a uniform proof theory for modal fixed point logics on 31 Janaury at 11:00 in the Aula.

The evet has received funding from the project number 617.001.857 of the Dutch Research Council NWO, and from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101064105.

When

On Monday 29 January from 9:00 - 17:00 and on Tuesday 30 January from 9:00 - 11:30.

Where

Room F0.01 at the Bushuis, Kloveniersburgwal 48. The room is on the ground floor, immediately on the left when you enter the building. The conference dinner is on Monday 29 January at 20:00, at the Tolhuistuin, IJpromenade 2.

Organisers

Marianna Girlando, Guillermo Menendez Turata and Jan Rooduijn

Registration

Registration is now closed. Please contact the organisers if you would like to join but have not yet registered.

Programme

Click on a row to see the title and abstract. Alexis Saurin's talk is unfortunately cancelled, and will be replaced by Nick Bezhanishvili's tallk.

Time	Speaker
Monday
09:00 - 09:45	Jan Rooduijn A cyclic proof system for Guarded Kleene Algebra with Tests Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about imperative while programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT makes ordinary sequents sufficient for achieving regular completeness, unlike with Kleene Algebra, where hypersequents are required. Moreover, proof search is in Co-NP, as opposed to the PSPACE complexity of proof search for Kleene Algebra. This talk is based on joined work with Dexter Kozen and Alexandra Silva.
09:45 - 10:15	Coffee break
10:15 - 11:00	Sebastian Enqvist The reset rule with ordinal variables and cuts Dam, Gurov & Sprenger have developed proof systems for modal and first-order mu-calculi using explicit variables for ordinal approximants of fixpoints. The annotated systems of Jungteerapanich and Stirling are similar, but use a different correctness criterion involving the so called "reset rule". Moreover, the latter systems are cut-free by design. I will show by an example that, in fact, combining the cut rule with a Jungteerapanich-Stirling-style reset rule results in an unsound system. Luckily, there is a simple fix which becomes apparent when considering the straightforward semantics of explicit ordinal variables. The result is a system which combines the virtues of both types of proof system: the presence of the cut rule allows us to capture the full strength of the Dam-Sprenger system for first-order mu-calculus, while the reset rule is advantageous in that it simplifies proof checking and helps with proof search. A recent application is a sound and complete, finitary (cyclic) proof system for the two-way mu-calculus. The talk will be based on joint work with Bahareh Afshari, Graham Leigh, Johannes Marti and Yde Venema.
11:00 - 11:45	Guillermo Menéndez Turata A cyclic proof system for intuitionistic linear-time temporal logic Intuitionistic linear-time temporal logic, iLTL, combines Pnueli’s linear-time temporal logic (LTL) and propositional intuitionistic logic. Models of iLTL are two-dimensional: every state has at least one temporal successor and zero or more intuitionistic ‘successors’. Monotonicity of the temporal successor function with respect to the intuitionistic order suffices to ensure that truth is preserved upwards intuitionistically. We provide a cut-free, finitary cyclic proof system for iLTL. The calculus uses labelled formulas in order to accommodate the interplay between the temporal and the intuitionistic dimensions.
11:45 - 13:30	Lunch
13:30 - 14:15	Thomas Studer Cut-elimination: old results and new questions We review some results about cut-elimination in infinitary systems, i.e. systems with infinitely branching rules, for modal fixed point logics. Then, we discuss recent approaches to cut-elimination in ill-founded and cyclic systems.
14:15 - 15:00	Nick Bezhanishvili The topological mu-calculus: completeness and the finite model property In this talk I will discuss a new method of proving completeness for a large class of transitive modal fixed-point logics. I will also review topological completeness of these logics with respect to the derived set semantics. This is joint work with Alexandru Baltag and David Fernandez Duque
15:00 - 15:30	Coffee break
15:30 - 16:15	Martin Lange Fixpoints in Modal Logic: Finite Convergence and Higher Order Fixpoint iteration is the main tool for evaluating recursively defined properties in temporal specification languages like the modal mu-calculus Lmu. Finite convergence, i.e. the phenomenon of reaching a fixpoint after finitely many iterations only, is of particular interest for algorithmic properties of such logics. The iteration of fixpoints of Lmu formulas trivially converges finitely on finite structures, but also clearly on (infinite) structures whose bisimulation quotient is finite. We start by reviewing the converse and present a (word) structure W on which all mu-calculus fixpoints converge finitely, even though that structure does not have a finite bisimulation quotient. We then introduce Higher-Order Fixpoint Logic HFL, an extension of Lmu in which formulas denote (higher-order) functions on sets of states of a transition system, with a type order such that Lmu is exactly HFL0, the set of HFL formulas only using functions of order 0. HFL is interesting in this context because it is very easy to construct an HFL1 formula, i.e. using first-order functions, that does not converge finitely over W. Moreover, it introduces a hierarchy of classes of transition systems with finite convergence of (higher-order) fixpoints. It is not unreasonable to suspect this hierarchy to collapse at a low type level, but this is currently an open question. We will present some ideas on how to tackle this. This is joint work with Florian Bruse and Marco Sälzer of the University of Kassel and Etienne Lozes of the Université Cote d'Azur.
20:00 -	Conference dinner
Tuesday
09:00 - 09:45	Johan van Benthem An Abstract Look at the Fixed-Point Theorem for Provability Logic I discuss some general perspectives on the well-known Fixed-Point Theorem for Provability Logic, taking my cues from an old abstract argument by Dick de Jongh. This will lead us into issues about recursion in several old and new modal logics.
09:45 - 10:30	Anupam Das Intuitionistic Gödel-Löb logic, à la Simpson We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, lIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL's usual frame condition, termination, is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that lIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL. This talk is based on joint work with Iris van der Giessen and Sonia Marin: https://arxiv.org/abs/2309.00532.

Questions?

Please contact the organisers by sending an email to name@uva.nl, where 'name' is in {m.girlando, g.m.t.menendezturata, j.m.w.rooduijn}.