Technische Universität
             Darmstadt leanCoP Logo Universität Potsdam

Lean Connection-Based Theorem Proving


  What is leanCoP?  
Download
Documentation
ileanCoP
MleanCoP
Contact
What is leanCoP?

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.

News: 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.    CASC-21 Trophy    

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.

Contact

Please let me know if you have any questions or if you have done something interesting with leanCoP.


Jens Otten · Institut für Informatik · University of Potsdam · 24.01.2012