--------------------------
nanoCoP ReadMe File (v2.0)
-----------
Description
nanoCoP is a compact non-clausal connection theorem prover
for classical first-order logic implemented in Prolog. See
web site at http://www.leancop.de/nanocop/ for more details.
--------
Contents
ReadMe_nanocop - this ReadMe file
nanocop.sh - shell script to invoke nanoCoP
nanocop20.pl - the nanoCoP 2.0 core prover
(nanocop20_swi.pl for SWI Prolog)
nanocop_main.pl - invokes the nanoCoP core prover
nanocop_proof.pl - presents proof found by nanoCoP
nanocop_tptp2.pl - translates problems from TPTP syntax
------------
Installation
Set the path for the Prolog system (ECLiPSe 5.x or SWI) and the
path for the nanoCoP prover in the file nanocop.sh. This file
also includes parameters to control the output of the proof and
to specify the proof layout.
---------
Execution
./nanocop.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: ./nanocop.sh SET/SET009+3 10
Output if formula is valid: %s is a Theorem
Output if formula is invalid: %s is a Non-Theorem
Example: SET/SET009+3 is a 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),
';' (disjunction), ',' (conjunction), '=>' (implication), '<=>'
(equivalence), and the logical quantifiers 'all X:' (universal)
and 'ex X:' (existential) where X is a Prolog variable.
Example: f( ((p , all X:(p=>q(X))) => q(a)) ).
Alternatively, the problem file may contain a formula in TPTP
syntax (see http://www.tptp.org). If the problem file contains
equality ('=') all equality axioms are added automatically.
-----------
At a Glance
System: nanoCoP
Version: 2.0
URL: http://www.leancop.de/nanocop/
Command: ./nanocop.sh %s %d
Format: leancop/nanocop or (raw) tptp
Output: - valid: %s is a Theorem
- invalid: %s is a Non-Theorem
- unsatisfiable(*): %s is Unsatisfiable
- satisfiable(*): %s is Satisfiable
(*: for problems in TPTP syntax without conjecture)