Technische Universität
             Darmstadt nanoCoP Logo University of Oslo

Non-clausal Connection-Based Theorem Proving


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

nanoCoP is a compact non-clausal automated theorem prover for classical first-order logic. It is based on the non-clausal connection calculus for classical logic. More details about the calculus can be found in the documentation.

Features of nanoCoP

  • Theorem prover for classical first-order logic with equality.
  • Based on the non-clausal connection calculus.
  • Proof search on the original formula structure.
  • Implemented in Prolog.
  • Sound and complete.
  • Decision procedure for propositional logic.
  • Strong performance.
  • Simple first-order form input format (leanCoP or TPTP).
  • Output of compact non-clausal connection proof.
  • Available under the GNU general public license.

Download

nanoCoP is optimized for the open source Prolog system ECLiPSe. It should run on other Prolog systems as well. The following package includes a ReadMe file containing more information.


Jens Otten · Institutt for informatikk · University of Oslo · 11.11.2016