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

Theorem prover for intuitionistic firstorder logic with equality.

Based on the intuitionistic nonclausal 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 nonclausal connection proof (v2.0).

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