Technische Universität
             Darmstadt nanoCoP Logo University of Oslo

Non-clausal Connection-Based Theorem Proving

  What is leanCoP?  
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.


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