----------------------------
nanoCoP-M ReadMe File (v1.0)
-----------
Description
nanoCoP-M is a compact non-clausal connection theorem prover for
the first-order modal logics D, T, S4, and S5 (with constant,
cumulative or varying domains) implemented in Prolog. See the
web site http://www.leancop.de/nanocop-m/ for more details.
--------
Contents
ReadMe_nanoCoP-M - this ReadMe file
nanocopm.sh - shell script to invoke nanoCoP-M
nanocopm.pl - the nanoCoP-M core prover
nanocopm_main.pl - invokes the nanoCoP-M core prover
nanocop_qmltp2.pl - translates problems that are in QMLTP syntax
------------
Installation
Set the path for the Prolog system (ECLiPSe 5.x) and the path
for the nanoCoP-M prover in the file nanocopm.sh. The modal
logic and domain condition are specified through the variables
LOGIC (d,t,s4,s5) and DOMAIN (const,cumul,vary).
---------
Execution
./nanocopm.sh %s
where %s is the name of the problem file.
Example: ./nanocopm.sh SYM/SYM002+1
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 built from 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 may contain a formula in QMLTP
syntax (see http://www.iltp.de/qmltp/).
-----------
At a Glance
System: nanoCoP-M
Version: 1.0
URL: http://www.leancop.de/nanocop-m/
Command: ./nanocopm.sh %s
Format: leancop/nanocop 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
(*: for problems in QMLTP syntax without conjecture)