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 documentation.

Features of nanoCoP-M

• Theorem prover for modal first-order 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 non-clausal connection calculus.
• Proof search on the original formula structure.
• Implemented in Prolog.
• Sound and complete.
• Leading performance.
• Simple input format (nanoCoP-M or QMLTP syntax).
• Output of readable non-clausal connection proof (v2.0).
• Available under the GNU general public license.

nanoCoP-M 2.0 contains several enhancements and optimizations of the basic non-clausal connection calculus, such as improved restricted backtracking and a strategy scheduling. nanoCoP-M 2.0 can output a detailed non-clausal connection proof in different formats, for example in a Prolog syntax or in a readable format.

nanoCoP-M 2.0 runs on ECLiPSe Prolog (5.x) and on SWI-Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running nanoCoP-M.

• nanoCoP-M20.tar.gz (tar/gzip, 11.5 kbytes)

nanoCoP-M 1.0 implements the basic non-clausal 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.

• nanoCoP-M.tar.gz (tar/gzip, 7 kbytes)

nanoCoP-M-DS5 is a version of leanCoP-M 2.0 that is optimized for the modal first-order logics D and S5.

nanoCoP-M-DS5 runs on ECLiPSe Prolog (5.x) and on SWI-Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running nanoCoP-M-DS5.

• nanoCoP-M-DS5_10.tar.gz (tar/gzip, 10.9 kbytes)