MleanCoP is a compact automated theorem prover for modal first-order logic based on the clausal connection calculus for modal logic. It extends the classical leanCoP prover by adding prefixes to the literals and a prefix unification algorithm.

Features of MleanCoP

• Theorem prover for modal first-order logic.
• For the modal logics D, T, S4, and S5.
• For heterogeneous multimodal logics (v1.3).
• For constant, cumulative and varying domains.
• Based on the modal connection calculus.
• Implemented in Prolog.
• Sound and complete.
• Leading performance.
• Simple input format (mleancop or modal TPTP syntax).
• Output of compact modal connection proof (v1.3).
• Available under the GNU general public license.

The QMLTP library contains performance results of MleanCoP and other theorem provers for modal logic.

MleanCoP 1.3 contains the following enhancements: support for heterogenous multimodal logics, output of a compact modal connection proof, support for the modal TPTP input syntax, improved strategy scheduling, and additional support for SWI and SICStus Prolog.

MleanCoP 1.3 runs on ECLiPSe Prolog (5.x), SWI Prolog and SICStus Prolog. It should run on most other Prolog systems as well. The ReadMe file contains more information on installing and running MleanCoP.

• mleancop13.tar.gz

MleanCoP 1.2 requires the open source Prolog system ECLiPSe. The following package includes a ReadMe file containing information about the syntax of MleanCoP. Descriptions and performance results of MleanCoP 1.2 can be found in the documentation.

• mleancop12.tar.gz

MleanCoP-DS5 is a version of MleanCoP 1.3 that is optimized for the modal first-order logics D and S5.

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

• MleanCoP-DS5_10.tar.gz