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

Original German Text




Other Material

Short submission and talk at AiML2020:

Tableau implementation in Haskell (Work in progress!)

Lean formalisation, only covering Basic Modal Logic so far: