


MleanSeP is a Prolog program that implements a very compact
theorem prover for some firstorder modal logics.
It is based on the standard modal sequent
calculi for modal logics. Using an analytic proof
search, free variables and a dynamic skolemization ensures
good performance.
Inference rules are defined in a modular way which makes
modifications to the calculus easily possible.
Features of MleanSeP

Theorem prover for the modal firstorder logics K, K4,
D, D4, S4 and T for constant and cumulative domains.

Based on the standard modal sequent calculi using free
termvariables and skolemization.

Sound and complete.

Source code available for popular
Prolog systems, including ECLiPSe Prolog, SWIProlog and
SICStus Prolog.

Simple modal firstorder form input format.
The following paper provides details about the implemented
sequent calculi and the source code of MleanSeP.
The source code of MleanSeP is available for
ECLiPSe Prolog,
SWIProlog 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 MleanSeP on your system.
The MleanSeP prover is invoked with
prove(F). where F
is a modal firstorder 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 MleanSeP.

ModLeanTAP
 a compact Prolog theorem prover for modal logics based on
analytic tableaux by Bernhard Beckert and Rajeev Goré.

leanCoP
 a compact Prolog theorem prover for classicalfirst order
logic.

ileanTAP
 a compact Prolog theorem prover for intuitionistic
firstorder logic based on analytic tableaux and
prefix unification.

leanTAP
 a compact Prolog theorem prover for firstorder 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.

ncDP
 a compact Prolog nonclausal "DavisPutnam" prover.
Please feel free to contact us if you have any
questions about MleanSeP. If you have any suggestions for improvements
or if you have done something interesting with MleanSeP, please
let us know about it.
