Tableau Calculus for PDL and Interpolation
This page provides the original German text of the diploma thesis Tableau-Kalkül für PDL und Interpolation by Manfred Borzechowski at FU Berlin in 1988, and an English translation by Malvin Gattinger. Please send any questions or comments to malvin@w4eg.eu.
Original German Text
Translation to English
Borzechowski1988-PDL-translation-Gattinger2020.pdf
Short talk at AiML2020
Follow-up
Article- Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Francisco Trucco Dalmas, Yde Venema: Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof. To appear in LMCS, 2026. arxiv.org/abs/2503.13276
- Basic Modal Logic in Lean 3: github.com/m4lvin/tablean
- PDL in Lean 4: github.com/m4lvin/lean4-pdl
