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