leanCoP 2.1 is the most recent version of leanCoP. Older versions are leanCoP 2.0 and leanCoP 1.0. Descriptions and performance results of these systems can be found in the documentation. Some references to work related to leanCoP are given below as well.

leanCoP 2.1 accepts TPTP input syntax, supports equality and outputs a connection proof. More information can be found in the documentation.

leanCoP 2.1 runs on ECLiPSe Prolog (5.x), SWI-Prolog or SICStus Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running leanCoP.

• leancop21.tar.gz

(As new versions of SWI-Prolog are not ISO compliant for certain predicates, please download the latest version of leanCoP 2.1 showing version "2.1(b)" in the header of the leancop.sh file.)

leanCoP-SInE combines the axiom selection system SInE with the leanCoP theorem prover. SInE is developed by Krystof Hoder. It is suitable for problems containing several thousands of axioms.

leanCoP-SInE requires Python and ECLiPSe Prolog (5.x), SWI-Prolog or SICStus Prolog. The following package includes a ReadMe file containing more information.

• leancop-sine21.tar.gz

leanCoP 2.0 contains the following enhancements of the basic calculus: regularity, lemmata, restricted backtracking, lean Prolog technology, a definitional clausal form translation, and a fixed strategy scheduling. Detailed information can be found in the documentation.

leanCoP 2.0 requires the open source Prolog system ECLiPSe. The following package includes a ReadMe file containing also information about the leanCoP input syntax.

• leancop20.tar.gz

The following small versions of the leanCoP 2.0 core prover are optimized for the size of the source code.

• leancop20_small_full.pl (ECLiPSe, 999 bytes)

  The core prover is invoked with "prove(M)." where M is a matrix, i.e. a list of clauses, and clauses are lists of literals where negation is expressed by "-". For example "prove([[q(a)], [-p], [p,-q(X)]])." will prove the validity (unsatisfiability) of the clause set {{q(a)}, {¬p}, {p,¬q(X)}}.

• leancop20_small.pl (ECLiPSe, 555 bytes)

  This program consists only of the actual search procedure. It is invoked with "prove(I,S)." where I is the maximum size of the active path, S is the set of settings, and the clauses are stored in Prolog's database. See the documentation for details.

randoCoP extends leanCoP 2.0 by integrating a technique that randomizes the proof search order. It is co-developed by Thomas Raths. randoCoP 1.1 accepts TPTP input syntax and outputs a connection proof. More information can be found in the leanCoP 2.0 documentation.

randoCoP requires the open source Prolog system ECLiPSe. The following package includes a ReadMe file containing more information.

• randocop11.tar.gz

leanCoP 1.0 implements the basic connection calculus. A detailed description can be found in the documentation.

The source code of leanCoP 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 information about the leanCoP input syntax.

• leancop.tar.gz (ECLiPSe 4.x)
  leancop_ec5.tar.gz (ECLiPSe 5.x)
  leancop_sicstus.tar.gz (SICStus)
  leancop_swi.tar.gz (SWI)

The following small versions of the leanCoP 1.0 prover are optimized for the size of the source code.

• leancop_small.pl (ECLiPSe 4.x, 333 bytes)
  leancop_small2.pl (ECLiPSe 5.x, SWI, SICStus, 395 bytes)

  The prover is invoked with "prove(M,I)." where M is a matrix, i.e. a list of clauses, and I is the maximum size of the active path. Clauses are lists of literals where negation is expressed by "-". For example "prove([[q(a)], [-p], [p,-q(X)]], 5)." will prove the validity (unsatisfiability) of the clause set {{q(a)}, {¬p}, {p,¬q(X)}}. Sound unification has to be switched on for the ECLiPSe 4.x version.

• veryleancop.pl (ECLiPSe 4.x, 199 bytes)

  This slightly restricted version of leanCoP is probably the smallest connection prover for classical first-order logic. It is invoked with "p(M,I)." where M is a list of clauses and I is the maximum size of the active path.

This is some work related to the leanCoP prover.

• lolliCoP is a reimplementation of leanCoP using the linear logic programming language Lolli. It is written by Joshua Hodas and Naoyuki Tamura.

• MaLeCoP extends leanCoP by integrating learning techniques. It is written by Josef Urban, Jiří Vyskočil and Petr Štěpánek.

• ileanCoP is a version of leanCoP for intuitionistic logic.

• MleanCoP is a version of leanCoP for modal logics.

• Other lean provers: leanTAP (classical first-order logic), ileanTAP and ileanSeP (intuitionistic first-order logic), ModLeanTAP (modal propositional logic), MleanTAP and MleanSeP (modal first-order logic), linTAP (multiplicative linear logic), ncDP (classical propositional logic).