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…