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 first-order intuitionistic logic.
MleanCoP is an extension of
leanCoP for several first-order modal logics.
MleanCoP 1.3 supports several
first-order multimodal logics and outputs a modal
+++ 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.