The QMLTP problem library for first-order modal logics. The Quantified Modal Logic Theorem Proving (QMLTP) library provides a platform for testing and evaluating automated theorem proving (ATP) systems for first-order modal logics. The main purpose of the library is to stimulate the development of new modal ATP systems and to put their comparison onto a firm basis. Version 1.1 of the QMLTP library includes 600 problems represented in a standardized extended TPTP syntax. Status and difficulty rating for all problems were determined by running comprehensive tests with existing modal ATP systems. In the presented version 1.1 of the library the modal logics K, D, T, S4 and S5 with constant, cumulative and varying domains are considered. Furthermore, a small number of problems for multi-modal logic are included as well.
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- 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)
- Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: Higher-order modal logics: automation and applications (2015)
- Steen, Alexander; Benzmüller, Christoph: There is no best (\beta)-normalization strategy for higher-order reasoners (2015)
- Otten, Jens: MleanCoP: a connection prover for first-order modal logic (2014)
- Benzmüller, Christoph; Raths, Thomas: HOL based first-order modal logic provers (2013)
- Benzmüller, Christoph; Otten, Jens; Raths, Thomas: Implementing and evaluating provers for first-order modal logics (2012)
- Raths, Thomas; Otten, Jens: The QMLTP problem library for first-order modal logics (2012)