

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 heterogeneous multimodal logics (v2.0).

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 readable nonclausal connection proof (v2.0).

Available under the GNU general public license.
nanoCoPM 2.0
contains several enhancements and optimizations of the basic
nonclausal connection calculus, such as improved restricted
backtracking and a strategy scheduling.
nanoCoPM 2.0
can output a detailed nonclausal connection proof in different
formats, for example in a Prolog syntax or in a readable format.
nanoCoPM 2.0 runs on
ECLiPSe Prolog
(5.x) and on
SWIProlog.
It should run on most other Prolog systems as well.
The ReadMe file
contains more information on installing and running nanoCoPM.
nanoCoPM 1.0 implements the basic nonclausal connection calculus
and a few optimizations. It runs on the open source Prolog system
ECLiPSe.
The following package includes a
ReadMe file containing
more information.
