ModLeanTAP is a lean Prolog implementation of a modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal variables), which has been developed by Bernhard Beckert and Rajeev Goré.
ModLeanTAP is not only surprisingly short, but compares favourably with other considerably more complex implementations for modal deduction.
ModLeanTAP's development was inspired by the lean tableau-based prover for first-order logic leanTAP.
ModLeanTAP Version 2.0 includes additional search space restrictions and fairness strategies, giving a decision procedure for the logics K, KD, KT, and S4.
Free Variable Tableaux for Propositional Modal Logics
Bernhard Beckert & Rajeev Goré
Proceedings, International Conference on Theorem Proving with Analytic
Tableaux and Related Methods, Pont-a-Mousson, France, 1997.
PDF
- BibTeX.
Free Variable Tableaux for Propositional Modal Logics (Extended Version)
Bernhard Beckert & Rajeev Goré
University of Karlsruhe, Department of Computer Science, TR 41/96.
PDF - BibTeX.
System Description: leanK 2.0
Bernhard Beckert & Rajeev Goré
Proceedings, International Conference on Automated Deduction
(CADE), Lindau, Germany, 1998.
PDF - BibTeX - Abstract - Springer Verlag, LNCS 1421.
leanK 2.0: Description for the Comparison of Theorem Provers for Modal Logics
Bernhard Beckert & Rajeev Goré;
Proceedings, International Conference on Theorem Proving
with Analytic Tableaux and Related Methods, Oisterwijk, The Netherlands, 1998.
PDF - BibTeX - Abstract - Springer Verlag, LNCS 1397.
ModLeanTAP is written in SICStus Prolog, but it can easily be adapted to other Prolog dialects; the only change that has to be made is the way in which the library functions append/3 and reverse/2 for lists are provided, that are used by ModLeanTAP.
Right now versions of ModLeanTAP are only available for the following four of the basic 15 modal logics (but versions for the other logics can easily be constructed):
| Logic | Version 1.0 | Version 2.0 (Decision Procedure) |
| K | modlean_k.pl | modlean_dec_k.pl |
| KD | modlean_kd.pl | modlean_dec_kd.pl |
| KT | modlean_kt.pl | modlean_dec_kt.pl |
| S4 | modlean_s4.pl | modlean_dec_s4.pl |
In addition, there is a program modleantest.pl, that contains a few examples for testing ModLeanTAP (unfortunately it is not well formatted yet). It makes use of the module nnf.pl to transform its examples into negation normal form.
A TAR file is available that contains all the above files.
Do not hesitate to contact us if you are looking for any information you cannot find on these pages, or should you have any further questions, suggestions, or comments.
| Bernhard
Beckert University of Koblenz Institute for Computer Science Universitätsstraße 1 56070 Koblenz, Germany Email: beckert@uni-koblenz.de Phone: +49 261 287-2775 |
Rajeev
Goré Automated Reasoning Group Australian National University Canberra, ACT, 0200, AUSTRALIA Email: Rajeev.Gore@anu.edu.au Phone: +61 6 279 8603 Fax: +61 6 279 8645 |
Maintainer: Bernhard Beckert