-------------------------------
MleanCoP-DS5 ReadMe File (v1.0)
-----------
Description
MleanCoP-DS5 is a theorem prover implemented in Prolog for the
first-order modal logics D and S5 (with constant, cumulative or
varying domains). See http://www.leancop.de/mleancop/ for details.
--------
Contents
ReadMe_mleancop-ds5 - this ReadMe file
mleancop-ds5.sh - shell script to invoke MleanCoP-DS5
mleancop_ds5_10.pl - the MleanCoP-DS5 core prover for ECLiPSe
(mleancop-ds5-10_swi.pl for SWI Prolog)
mleancop_defmm.pl - clausal form transformation
mleancop_ds5_main.pl - invokes the MleanCoP-DS5 core prover
mleancop_tptp2.pl - translates problems in modal TPTP syntax
------------
Installation
Set the path for the Prolog system (ECLiPSe or SWI Prolog) and
the path for the MleanCoP-DS5 prover in the file mleancop-ds5.sh.
Modal logic and domain condition are specified by the variables
LOGIC (d,s5) and DOMAIN (const,cumul,vary). This file also includes
parameters to control the proof output.
---------
Execution
./mleancop-ds5.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds.
Example: ./mleancop-ds5.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 (s5/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)))) ).
Alternatively, the problem file can contain a formula in the
QMLTP syntax (see http://www.iltp.de/qmltp/).
-----------
At a Glance
System: MleanCoP-DS5
Version: 1.0
URL: http://www.leancop.de/mleancop/
Command: ./mleancop-ds5.sh %s %d
Format: mleancop or QMLTP
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)