|
|
|
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.
|
News:
MleanCoP 1.3 supports several
first-order multimodal logics and outputs a modal
connection proof
+++ leanCoP-Ω wins new (demo) TFA division (Typed
First-order logic with Arithmetic) at the CADE System Competition
CASC-J5
(press
release)
+++ leanCoP 2.1 ranked third of the provers that output
a proof in the core FOF division at the CADE System Competition
CASC-22
+++ 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
CASC-J4
+++ leanCoP 2.0 wins "Best Newcomer" award at
the CADE System Competition
CASC-21.
|
|
|
|
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.
-
Strong performance.
-
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.
|
Lean Connection-Based Theorem Proving