ileanCoP is a compact automated theorem prover
for intuitionistic first-order logic based on the clausal
connection calculus for intuitionistic logic.
It extends the classical leanCoP prover by adding prefixes
to the literals and a prefix unification algorithm.
More details about the calculus can be found in the
Features of ileanCoP
Theorem prover for intuitionistic first-order logic.
Based on the intuitionistic connection calculus.
Implemented in Prolog.
Sound and complete.
Simple first-order form input format.
Available under the GNU general public license.
The ILTP library contains
performance results of ileanCoP and other
theorem provers for intuitionistic logic.
There are two versions of ileanCoP available: ileanCoP 1.2 and
ileanCoP 1.2 contains the following enhancements:
regularity, lemmata, restricted backtracking, lean
Prolog technology, and a definitional clausal form translation.
Descriptions and performance results of both
systems can be found in the
ileanCoP 1.2 requires the open source Prolog system
The following package includes a
ReadMe file containing
information about the syntax of ileanCoP.
The source code of ileanCoP 1.0 is available for
SICStus Prolog. It
should run on most other Prolog systems as well.
The ReadMe file
contains more information.