Modal Tableau with Interpolation in Haskell
GPL-3.0 License
Goal: a tableau prover for propositional logic, the basic modal logic K and propositional dynamic logic (PDL). The prover should also find interpolants, following the method described by Manfred Borzechowski in 1988. See https://malv.in/2020/borzechowski-pdl/ for the original German text and an English translation.
There are two different provers: one based on lists. and a proper tableau.
Interpolation is also implemented twice: once replacing atoms by constants as described in Wikipedia: Craig interpolation, and using the tableaux.
stack ghci src/Logic/BasicModal/Prove/Tree.hs
λ> provable (Box (p --> q) --> (Box p --> Box q))
True
λ> provable (p --> Box p)
False
stack ghci src/Logic/BasicModal/Interpolation/ProofTree.hs
λ> let (f,g) = ( Box ((At 'p') --> (At 'q')) , (Neg (Box ((At 's') --> (At 'q')))) --> (Neg (Box (At 'p'))) )
λ> mapM_ (putStrLn .ppForm) [f, g]
☐¬(p & ¬q)
¬(¬☐¬(s & ¬q) & ¬¬☐p)
λ> interpolateShow (f,g)
Showing tableau with GraphViz ...
Interpolant: ☐¬(¬¬p & ¬¬¬q)
Simplified interpolant: ☐¬(p & ¬q)
The last command will also show this tableau:
See the test file for more examples, including interpolation and consistency checks.
Public web interface: https://w4eg.de/malvin/illc/tapdleau/
To run the web interface locally do stack build
and then stack exec tapdleau
.
For developing you can recompile and restart the web interface on any code changes Like this:
stack build --file-watch --exec "bash -c \"pkill tapdleau; stack exec tapdleau &\""
Use stack test
to run all tests from the test folder.
For PDL we also use the files formulae_exp_unsat.txt and formulae_exp_sat.txt from http://users.cecs.anu.edu.au/~rpg/PDLComparisonBenchmarks/. Note: The files have been modified to use star as a postfix operator.
Prover:
unravel
instead.Technical debt:
Interpolation:
Bonus Information:
These are not needed to define interpolants, but part of the proof the definition is correct.
Testing:
Semantics:
Nice to have UX/UI:
Rejected ideas:
(TableauIP, Path)
pairs?Rajeev Goré and Florian Widmann (2009): An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. https://doi.org/10.1007/978-3-642-02959-2_32
Roman Kuznets (2015): Craig Interpolation via Hypersequents. https://sites.google.com/site/kuznets/interpol_hyper_v2.pdf
Francesca Perin (2019): Implementing Maehara's Method for Star-Free Propositional Dynamic Logic. https://fse.studenttheses.ub.rug.nl/20770/ https://github.com/FrancescaPerin/BScProject
Other PDL provers are mentioned at http://www.cs.man.ac.uk/~schmidt/tools/.