
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
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.
nanoCoPMDS5 is a version of leanCoPM 2.0 that is optimized for the modal firstorder logics D and S5. nanoCoPMDS5 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 nanoCoPMDS5.

Jens Otten · Institutt for informatikk · University of Oslo · 05.05.2022 