leanCoP is a compact automated theorem prover for classical
first-order logic. It is based on the connection calculus and
implemented in Prolog.
ileanCoP is an extension of
leanCoP for intuitionistic first-order logic.
MleanCoP is an extension of
leanCoP for several modal first-order logics.
leanCoP-Ω wins new (demo) TFA division (Typed First-order
logic with Arithmetic) at the CADE System Competition
+++ leanCoP 2.1 ranked third of the provers that output
a proof in the core FOF division at the CADE System Competition
+++ leanCoP-SInE 2.1 wins third place in the proof
class of the 2009
SUMO reasoning prize
+++ randoCoP 1.1 ranked third of the
provers that output a proof in the core FOF division
at the CADE System Competition
+++ leanCoP 2.0 wins "Best Newcomer" award at
the CADE System Competition
Features of leanCoP
Theorem prover for classical first-order logic with equality.
Based on the connection (tableau) calculus.
Implemented in Prolog.
Size of core prover: 333/555 bytes (v1.0/v2.0).
Sound and complete.
Decision procedure for propositional logic.
Simple first-order form input format (leanCoP or TPTP).
Output of readable connection proof (from v2.1).
Available under the GNU general public license.
Please let me know if you have any questions
or if you have done something interesting with leanCoP.