MleanCoP: a connection prover for first-order modal logic. 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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
- Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
- Steen, Alexander; Benzmüller, Christoph: The higher-order prover Leo-III (2018)
- Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph: Theorem provers for every normal modal logic (2017)
- Otten, Jens: nanoCoP: a non-clausal connection prover (2016)
- Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: Higher-order modal logics: automation and applications (2015)
- Demri, Stéphane (ed.); Kapur, Deepak (ed.); Weidenbach, Christoph (ed.): Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19--22, 2014. Proceedings (2014)
- Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)