Technische Universität
             Darmstadt leanCoP Logo University of Oslo

Lean Connection-Based Theorem Proving

  What is leanCoP?  

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.

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.

Jens Otten · Institutt for informatikk · University of Oslo · 11.11.2016