--------------------------------
nanoCoP-M-DS5 ReadMe File (v1.0)
-----------
Description
nanoCoP-M-DS5 is a compact non-clausal connection theorem prover
for the first-order modal logics D and S5 (with constant, cumulative
or varying domains) implemented in Prolog. See the web site at
http://www.leancop.de/nanocop-m/ for more details.
--------
Contents
ReadMe_nanoCoP-M-DS5 - this ReadMe file
nanocopm-ds5.sh - shell script to invoke nanoCoP-M-DS5
nanocopm_ds5_10.pl - the nanoCoP-M-DS5 core prover
(nanocopm_ds5_10_swi.pl for SWI Prolog)
nanocopm_ds5_main.pl - invokes the nanoCoP-M-DS5 core prover
nanocopm_proof.pl - presents proof found by nanoCoP-M-DS5
nanocop_qmltp2.pl - translates problems that are in QMLTP syntax
------------
Installation
Set the path for the Prolog system (ECLiPSe 5.x or SWI) 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,s5) and DOMAIN (const,cumul,vary). This file also includes
parameters to control the output of the proof and to specify the
proof layout.
---------
Execution
./nanocopm-ds5.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds (used for the internal strategy scheduling).
Example: ./nanocopm-ds5.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 (s5cumul) 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-DS5
Version: 1.0
URL: http://www.leancop.de/nanocop-m/
Command: ./nanocopm-ds5.sh %s %d
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)