ModLeanTAP: Lean Tableau-based Deduction for Propositional Modal Logics

INDEX: what is ModLeanTAP? papers source code contact address links

What is ModLeanTAP?

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.

Papers on ModLeanTAP and its Calculus

Source Code for ModLeanTAP

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)

In addition, there is a program, that contains a few examples for testing ModLeanTAP (unfortunately it is not well formatted yet). It makes use of the module to transform its examples into negation normal form.

A TAR file is available that contains all the above files.

Please Contact Us

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
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

Links to Related Pages

INDEX: what is ModLeanTAP? papers source code contact address links

Maintainer: Bernhard Beckert