MleanSeP: A Modal Sequent Prover What is MleanSeP? · Documentation · Source Code · Related Links · Contact Us Potsdam University Computer Science Theoretical CS
 What is MleanSeP?

MleanSeP is a Prolog program that implements a very compact theorem prover for some first-order 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 first-order logics K, K4, D, D4, S4 and T for constant and cumulative domains.
• Based on the standard modal sequent calculi using free term-variables and skolemization.
• 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 following paper provides details about the implemented sequent calculi and the source code of MleanSeP.

• Not available yet.

 Source Code

The MleanSeP 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 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 classical-first order logic.
• ileanTAP - a compact Prolog theorem prover for intuitionistic first-order logic based on analytic tableaux and prefix unification.
• 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.
• ncDP - a compact Prolog non-clausal "Davis-Putnam" prover.