nanoCoP-M is a compact automated theorem prover
for modal first-order logic. It is based on the non-clausal
connection calculus for modal logic and extends the
classical nanoCoP prover.
More details about the calculus can be found in the
Features of nanoCoP-M
Theorem prover for modal first-order logic.
Supports the modal logics D, T, S4, and S5.
Supports constant, cumulative, and varying domains.
Based on the modal non-clausal connection calculus.
Proof search on the original formula structure.
Implemented in Prolog.
Sound and complete.
Simple input format (nanoCoP-M or QMLTP syntax).
Output of compact modal non-clausal connection proof.
nanoCoP-M 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