University of Oslo nanoCoP Logo

Non-clausal Connection-Based Theorem Proving

  What is leanCoP?  
What is nanoCoP-i?

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

Features of nanoCoP-i

  • Theorem prover for intuitionistic first-order logic with equality.
  • Based on the intuitionistic non-clausal connection calculus.
  • Proof search on the original formula structure.
  • Implemented in Prolog.
  • Sound and complete.
  • Leading performance.
  • Simple input format (nanoCoP or TPTP syntax).
  • Output of readable non-clausal connection proof (v2.0).
  • Available under the GNU general public license.

nanoCoP-i 2.0

nanoCoP-i 2.0 contains several enhancements and optimizations of the basic non-clausal connection calculus, such as improved restricted backtracking and a strategy scheduling. nanoCoP-i 2.0 can output a detailed non-clausal connection proof in different formats, for example in a Prolog syntax or in a readable format.

nanoCoP-i 2.0 runs on ECLiPSe Prolog (5.x) and on SWI-Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running nanoCoP-i.

nanoCoP-i 1.0

nanoCoP-i 1.0 implements the basic non-clausal connection calculus and a few optimizations. It runs on the open source Prolog system ECLiPSe. The following package includes a ReadMe file containing more information.

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