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 documentation.

Features of ileanCoP

• Theorem prover for intuitionistic first-order logic.
• Based on the intuitionistic connection calculus.
• Implemented in Prolog.
• Sound and complete.
• Leading performance.
• 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.0. 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 documentation.

ileanCoP 1.2 requires the open source Prolog system ECLiPSe. The following package includes a ReadMe file containing information about the syntax of ileanCoP.

• ileancop12.tar.gz

The source code of ileanCoP 1.0 is available for ECLiPSe Prolog, SWI-Prolog and SICStus Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information.

• ileancop.tar.gz (ECLiPSe)
  ileancop_sicstus.tar.gz (SICStus)
  ileancop_swi.tar.gz (SWI)