We formalise a tableau system for modal logic, with the goal to prove soundness, completeness and Craig Interpolation.

For now we only consider the basic modal logic K, but the (very) long term goal is Propositional Dynamic Logic (PDL). We try to follow the definitions and ideas from Borzechowski (1988/2020).

Click here to open this repository in your browser via GitPod.

First install Lean and tools: https://leanprover-community.github.io/get_started.html

Then do this:

leanproject get m4lvin/tablean
cd tablean
leanproject build

• Soundness
• Completeness
• Interpolation

Module dependency overview:

• https://github.com/ljt12138/Formalization-PAL — see also https://arxiv.org/abs/2012.09388

• https://github.com/paulaneeley/modal — see also https://www.youtube.com/watch?v=kXCB5wzQTKc

• https://github.com/minchaowu/ModalTab — see also https://doi.org/10.4230/LIPIcs.ITP.2019.31

• https://github.com/bbentzen/mpl/ — see also https://arxiv.org/abs/1910.01697

• https://github.com/LudvikGalois/coq-CPL-NNF-tableau

• https://github.com/m4lvin/modal-tableau-interpolation

• https://github.com/FrancescaPerin/BScProject — see also https://fse.studenttheses.ub.rug.nl/20770/

For their helpful advice and code hints I would like to thank Alex J. Best, Emma Brakkee, Jasmin Blanchette, Riccardo Brasca, Kevin Buzzard, Mario Carneiro, Yaël Dillies, Patrick Johnson, Kyle Miller, Eric Rodriguez, Ruben Van de Velde, Eric Wieser, and all other friendly people at leanprover.zulipchat.com.