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é
Studia Logica, 69:1, p. 59-96, 2001.
PDF
- BibTeX.
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 Karlsruhe Institute of Technology Department of Informatics Am Fasanengarten 5 76131 Karlsruhe, Germany Email: beckert@kit.edu |
Rajeev
Goré Logic and Computation Group Research School of Computer Science ANU College of Engineering and Computer Science The Australian National University Canberra ACT 0200, AUSTRALIA Email: Rajeev.Gore@anu.edu.au |
Maintainer: Bernhard Beckert