27 citations · 83 across the 25 of their papers we have counts for
25 papers · 1 filter
Interpolation for Converse PDL
Johannes Kloibhofer, Valentina Trucco Dalmas, Yde Venema
Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation…
Interpolation for the two-way modal mu-calculus
Johannes Kloibhofer, Yde Venema
The two-way modal mu-calculus is the extension of the (standard) one-way mu-calculus with converse (backward-looking) modalities. For this logic we introduce two new sequent-style…
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen +3
We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later crit…
Proof Systems for the Modal -Calculus Obtained by Determinizing Automata
Maurice Dekker, Johannes Kloibhofer, Johannes Marti +1
Automata operating on infinite objects feature prominently in the theory of the modal -calculus. One such application concerns the tableau games introduced by Niwiński & Walukie…
Focus-style proofs for the two-way alternation-free -calculus
Jan Rooduijn, Yde Venema
We introduce a cyclic proof system for the two-way alternation-free modal -calculus. The system manipulates one-sided Gentzen sequents and locally deals with the backwards modal…
Filtration and canonical completeness for continuous modal mu-calculi
Jan Rooduijn, Yde Venema
The continuous modal mu-calculus is a fragment of the modal mu-calculus, where the application of fixpoint operators is restricted to formulas whose functional interpretation is Sc…