3 papers
cs.LO2025
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…
cs.LO2025
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…
cs.LO2025
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen +4
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…