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
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.
Simple first-order form input format (leanCoP or TPTP).
Output of readable non-clausal connection proof (v2.0).
Available under the GNU general public license.
contains several enhancements and optimizations of the basic
non-clausal connection calculus, such as improved restricted
backtracking and a strategy scheduling.
can output a detailed non-clausal connection proof in different
formats, for example in a Prolog syntax or in a readable format.
nanoCoP 2.0 runs on
(5.x) and on
It should run on most other Prolog systems as well.
The ReadMe file
contains more information on installing and running nanoCoP.
nanoCoP 1.0 implements the basic non-clausal connection calculus
and a few optimizations. It runs on the open source Prolog system
The following package includes a
ReadMe file containing