nanoCoP is a compact nonclausal automated theorem prover
for classical firstorder logic. It is based on the nonclausal
connection calculus for classical logic.
More details about the calculus can be found in the
documentation.
Features of nanoCoP

Theorem prover for classical firstorder logic with equality.

Based on the nonclausal connection calculus.

Proof search on the original formula structure.

Implemented in Prolog.

Sound and complete.

Decision procedure for propositional logic.

Strong performance.

Simple firstorder form input format (leanCoP or TPTP).

Output of readable nonclausal connection proof (v2.0).

Available under the GNU general public license.
nanoCoP 2.0
contains several enhancements and optimizations of the basic
nonclausal connection calculus, such as improved restricted
backtracking and a strategy scheduling.
nanoCoP 2.0
can output a detailed nonclausal connection proof in different
formats, for example in a Prolog syntax or in a readable format.
nanoCoP 2.0 runs on
ECLiPSe Prolog
(5.x) and on
SWIProlog.
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 nonclausal 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.
