Propositional Dynamic Logic in Lean 4
Project Goal
The aim is to prove that Propositional Dynamic Logic (PDL) has the Craig Interpolation property. The main reference is the following.
- Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Valentina Trucco Dalmas, Yde Venema: Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof. Preprint 2025, https://arxiv.org/abs/2503.13276
The article contains direct links to the corresponding parts of the formalization here.
A checkmark in the article means that the Lean statement is sorry-free, including all its dependencies.
There is no separate blueprint.
Useful Links
-
Documentation: https://m4lvin.github.io/lean4-pdl/docs/ (generated by doc-gen4)
-
Tableaux prover: https://w4eg.de/malvin/illc/tapdleau (implemented here in Haskell, useful to run examples)
-
Open this repository in Gitpod or GitHub Codespaces
Module dependency overview
(Run make dependencies.svg to update this.)
Other References
- https://github.com/m4lvin/tablean - previous project for Basic Modal Logic, in Lean 3. Code from there has been ported to Lean 4 and is included here in the
Bmlfolder. - https://malv.in/2020/borzechowski-pdl - the German original proof by Borzechowski (1988) and the English translation (2020)