

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

Available under the GNU general public license.
nanoCoP 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.
