--------------------
MleanCoP ReadMe File
-----------
Description
MleanCoP is a theorem prover for the modal first-order logics
D, T, S4 and S5 (with constant, cumulative or varying domains)
implemented in Prolog. See http://www.leancop.de for more details.
--------
Contents
ReadMe_mleancop - this ReadMe file
mleancop.sh - shell script to invoke MleanCoP
mleancop12.pl - the MleanCoP core prover
def_mm_modal.pl - clausal form transformation
leancop_tlimit - invokes MleanCoP with a time limit
format.leancop - format file for the TPTP2X tool
------------
Installation
Set the path for the ECLiPSe Prolog system (version 5 or greater)
and the path for the MleanCoP prover in the file mleancop.sh.
Modal logic and domain condition are specified by setting the
variables LOGIC (d,t,s4,s5) and DOMAIN (const,cumul,vary).
---------
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 600
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().
in which is a 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)))) ).
--------------
Transformation
Problems in the modal TPTP syntax are translated into the (modal)
leanCoP format by using the TPTP2X tool.
Format file: format.mleancop
Options: stdfof
Example: ./tptp2X -f mleancop -t stdfof SYM/SYM002+1.p
-----------
At a Glance
System: MleanCoP
Version: 1.2
URL: http://www.leancop.de/mleancop/
Command: ./mleancop.sh %s %d
Format: leancop
Transform: stdfof
Proved: %s is a Modal () Theorem
Refuted: %s is a Modal () Non-Theorem
(where is the selected modal logic and domain condition)