MleanTAP: A Modal Theorem Prover

Universität Potsdam

What is MleanTAP?
 · Documentation
 · Source Code
 · Related Links
 · Contact Us
Potsdam University
Computer Science
Theoretical CS
What is MleanTAP?

MleanTAP is a Prolog program that implements a sound and complete theorem prover for some first-order modal logics. It is based on free-variable semantic tableaux extended by an additional prefix unification to ensure the particular restrictions in modal logics.

Features of MleanTAP

  • Theorem prover for the modal first-order logics D, T, S4, and S5 for constant, cumulative and varying domains.
  • Based on a free-variable semantic tableau calculus.
  • Sound and complete.
  • Source code available for popular Prolog systems, including ECLiPSe Prolog, SWI-Prolog and SICStus Prolog.
  • Simple modal first-order form input format.


The short paper contains a description of the source code and some performance results achieved with MleanTAP.

  • Not available yet.

Source Code

The source code of MleanTAP is available for ECLiPSe Prolog, SWI-Prolog and SICStus Prolog; it should run on most other Prolog systems as well. Please contact us if you encounter any problems when downloading or running MleanTAP on your system.

The MleanTAP prover is invoked with  prove(F).  where  F  is a modal first-order formula. For example  prove( all X: ex Y:(~ *q, #p(Y)=>p(X)) ).  will prove the validity of the given formula. The logical connectives are expressed by "#" (modal box operator), "*" (modal diamond operator), "~" (negation), "," (conjunction), ";" (disjunction), "=>" (implication), "<=>" (equivalence); quantifiers are expressed by "all X:" (universal) and "ex X:" (existential).

Related Links

Here is a selection of links related to MleanTAP.

  • ModLeanTAP - a compact Prolog theorem prover for modal logics based on analytic tableaux by Bernhard Beckert and Rajeev Goré.
  • leanTAP - a compact Prolog theorem prover for first-order logic based on analytic tableaux by Bernhard Beckert and Joachim Posegga.
  • linTAP - a compact Prolog theorem prover for the multiplicative and exponential fragment of Girard's linear logic.
  • leanCoP - a compact Prolog theorem prover for classical-first order logic.
  • ncDP - a compact Prolog non-clausal "Davis-Putnam" prover.

Contact Us

Please feel free to contact us if you have any questions about MleanTAP. If you have any suggestions for improvements or if you have done something interesting with MleanTAP, please let us know about it.

Jens Otten · Institut für Informatik · University of Potsdam · 30.08.2011