MleanCoP swMATH ID: 21522 Software Authors: Otten, Jens Description: 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. Homepage: http://www.leancop.de/mleancop/ Related Software: QMLTP; TPTP; E Theorem Prover; ileanCoP; leanCoP; Leo-III; FEMaLeCoP; VAMPIRE; Nitpick; nanoCoP; Isabelle/HOL; GitHub; leanTAP; Satallax; MSPASS; SPASS; LoTREC; ENIGMA; MaLeCoP; PicoSAT Cited in: 15 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year MleanCoP: a connection prover for first-order modal logic. Zbl 1423.68423Otten, Jens 2014 all top 5 Cited by 20 Authors 4 Benzmüller, Christoph Ewald 4 Steen, Alexander 3 Otten, Jens 2 Dixon, Clare 2 Hustadt, Ullrich 2 Libal, Tomer 2 Nalon, Cláudia 2 Papacchini, Fabio 2 Urban, Josef 1 Brown, Chad Edward 1 Demri, Stéphane P. 1 Färber, Michael 1 Gleißner, Tobias 1 Kaliszyk, Cezary 1 Kapur, Deepak 1 Rawson, Michael 1 Reger, Giles 1 Weidenbach, Christoph 1 Woltzenlogel Paleo, Bruno 1 Zombori, Zsolt Cited in 2 Serials 3 Journal of Automated Reasoning 1 Lecture Notes in Computer Science Cited in 3 Fields 15 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Citations by Year