nanoCoP: a non-clausal connection prover. nanoCoP is a compact non-clausal automated theorem prover for classical first-order logic. It is based on the non-clausal connection calculus for classical logic. More details about the calculus can be found in the documentation. Features of nanoCoP: Theorem prover for classical first-order logic with equality. Based on the non-clausal connection calculus. Proof search on the original formula structure. Implemented in Prolog. Sound and complete. Decision procedure for propositional logic. Strong performance. Simple first-order form input format (leanCoP or TPTP). Output of compact non-clausal connection proof. Available under the GNU general public license.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element