--------------------
ileanCoP ReadMe File
-----------
Description
ileanCoP is a theorem prover for intuitionistic first-order logic
implemented in Prolog. See http://www.leancop.de for more details.
--------
Contents
ReadMe_ileancop - this ReadMe file
ileancop.sh - shell script to invoke ileanCoP
ileancop12.pl - the ileanCoP core prover
def_mm_intu.pl - clausal form transformation
leancop_tlimit - invokes ileanCoP with a time limit
format.leancop - format file for the TPTP2X tool
------------
Installation
Set the path for the ECLiPSe Prolog system (version 5 or greater)
and the path for the ileanCoP prover in the file ileancop.sh.
---------
Execution
./ileancop.sh %s [%d]
where %s is the name of the problem file and %d is the (optional)
time limit in seconds.
Example: ./ileancop.sh SET/SET009+3 600
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 made up of 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)) ).
--------------
Transformation
Problems in the TPTP syntax are translated into the leanCoP format
by using the TPTP2X tool.
Format file: format.leancop
Options: stdfof+add_equality
Example: ./tptp2X -f leancop -t stdfof+add_equality SET/SET009+3.p
-----------
At a Glance
System: ileanCoP
Version: 1.2
URL: http://www.leancop.de/ileancop/
Command: ./ileancop.sh %s %d
Format: leancop
Transform: stdfof+add_equality
Proved: %s is an Intuitionistic Theorem
Refuted: %s is an Intuitionistic Non-Theorem