2 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
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…