---------------------------
MleanCoP ReadMe File (v1.3)
-----------
Description
MleanCoP is a theorem prover implemented in Prolog for the
first-order modal logics D, T, S4, and S5 (with constant,
cumulative or varying domains) and heterogeneous multimodal
logics. See http://www.leancop.de for details.
--------
Contents
ReadMe_mleancop - this ReadMe file
mleancop.sh - shell script to invoke MleanCoP
mleancop12.pl - the MleanCoP core prover for ECLiPSe
(mleancop13_swi/sic.pl for SWI/SICStus)
mleancop_defmm.pl - clausal form transformation
mleancop_main.pl - invokes the MleanCoP core prover
mleancop_tptp2.pl - translates problems in modal TPTP syntax
------------
Installation
Set the path for the Prolog system (ECLiPSe, SICStus or SWI)
and the path for the MleanCoP prover in the file mleancop.sh.
Modal logic and domain condition are specified by the variables
LOGIC (d,t,s4,s5,multi) and DOMAIN (const,cumul,vary). This
file also includes parameters to control the proof output.
---------
Execution
./mleancop.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds.
Example: ./mleancop.sh SYM/SYM002+1 10
Output if formula is valid: %s is a modal () Theorem
Output if formula is invalid: %s is a modal () Non-Theorem
where is the selected modal logic and domain condition.
Example: SYM/SYM002+1 is a modal (s4/cumul) Theorem
------
Syntax
The problem file has to contain a Prolog term of the form
f().
where is a modal first-order formula made up of Prolog
terms (atomic formulae), the logical connectives '~' (negation),
'#' (box operator), '*' (diamond operator), ';' (disjunction),
',' (conjunction), '=>' (implication), '<=>' (equivalence),
and the logical quantifiers 'all X:' (universal) and 'ex X:'
(existential) where X is a Prolog variable.
Example: f( ((# (all X: p(X))) => (all X: (# p(X)))) ).
For multimodal logic each modal operator is indexed with a Prolog
term and a modal logic (d,t,s4,s5).
Example: f( ((# 1^s4: p) => ((# 1^s4: p) ; (* 2^s5: q))) ).
Alternatively, the problem file can contain a formula in the
modal TPTP syntax (see http://www.iltp.de/qmltp/).
-----------
At a Glance
System: MleanCoP
Version: 1.3
URL: http://www.leancop.de/mleancop/
Command: ./mleancop.sh %s %d
Format: mleancop or modal tptp
Output: - valid: %s is a modal () Theorem
- invalid: %s is a modal () Non-Theorem
- unsatisfiable(*): %s is modal () Unsatisfiable
- satisfiable(*): %s is modal () Satisfiable
(where is the selected modal logic and domain condition)
(*: for problems in modal TPTP syntax without conjecture)