nanoCoP-i is a compact automated theorem prover
for intuitionistic first-order logic. It is based on the non-clausal
connection calculus for intuitionistic logic and extends the
classical nanoCoP prover.
More details about the calculus can be found in the
Features of nanoCoP-i
Theorem prover for intuitionistic first-order logic with equality.
Based on the intuitionistic non-clausal connection calculus.
Proof search on the original formula structure.
Implemented in Prolog.
Sound and complete.
Simple input format (nanoCoP or TPTP syntax).
Output of compact intuitionistic non-clausal connection proof.
nanoCoP-i 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