----------------------------
nanoCoP-i ReadMe File (v2.0)
-----------
Description
nanoCoP-i is a compact non-clausal connection theorem prover for
intuitionstic first-order logic implemented in Prolog. See the
web site at http://www.leancop.de/nanocop-i/ for more details.
--------
Contents
ReadMe_nanoCoP-i - this ReadMe file
nanocopi.sh - shell script to invoke nanoCoP-i
nanocopi20.pl - the nanoCoP-i core prover
(nanocopi20_swi.pl for SWI Prolog)
nanocopi_main.pl - invokes the nanoCoP-i core prover
nanocopi_proof.pl - presents proof found by nanoCoP-i
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-i prover in the file nanocopi.sh. This file
also includes parameters to control the output of the proof and
to specify the proof layout.
---------
Execution
./nanocopi.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: ./nanocopi.sh SET/SET009+3 10
Output if formula is valid: %s is an intuitionistic Theorem
Output if formula is invalid: %s is an intuitionistic Non-Theorem
Example: SET/SET009+3 is an intuitionistic 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-i
Version: 2.0
URL: http://www.leancop.de/nanocop-i/
Command: ./nanocopi.sh %s %d
Format: leancop/nanocop or (raw) tptp
Output: - valid: %s is an intuitionistic Theorem
- invalid: %s is an intuitionistic Non-Theorem