## MleanTAP: A Modal Theorem Prover 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.

 Documentation

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

• Not available yet.

 Source Code

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

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.