Abstract
MleanCoP is a fully automated theorem prover for first-order modal logic. The proof search is based on a prefixed connection calculus and an additional prefix unification, which captures the Kripke semantics of different modal logics. MleanCoP is implemented in Prolog and the source code of the core proof search procedure consists only of a few lines. It supports the standard modal logics D, T, S4, and S5 with constant, cumulative, and varying domain conditions. The most recent version also supports heterogeneous multimodal logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance of MleanCoP. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Otten, J. (2014). MleanCoP: A connection prover for first-order modal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8562 LNAI, pp. 269–276). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
