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
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.
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.
MleanCoP-DS5 is a version of MleanCoP 1.3 that is optimized for the modal first-order logics D and S5.
|Jens Otten · Institutt for informatikk · University of Oslo · 5.5.2022|