

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

Theorem prover for modal firstorder logic.

Supports the modal logics D, T, S4, and S5.

Supports constant, cumulative, and varying domains.

Based on the modal nonclausal connection calculus.

Proof search on the original formula structure.

Implemented in Prolog.

Sound and complete.

Leading performance.

Simple input format (nanoCoPM or QMLTP syntax).

Output of compact modal nonclausal connection proof.
nanoCoPM 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.
