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