Technische Universität
             Darmstadt leanCoP Logo University of Oslo

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 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.    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 · Institutt for informatikk · University of Oslo · 11.11.2016