

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 compact intuitionistic nonclausal connection proof.
nanoCoPi 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.
