Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Balsiger, P., Heuerding, A., Schwendimann, S.: A Benchmark Method for the Propositional Modal Logics K, KT, S4. Journal of Automated Reasoning 24, 297–317 (2000)
Benzmüller, C.E., Paulson, L.C: Quantified Multimodal Logics in Simple Type Theory. Seki Report SR-2009-02, Saarland University (2009) ISSN 1437-4447
Benzmüller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)
Blackburn, P., van Bentham, J., Wolter, F.: Handbook of Modal Logic. Elsevier, Amsterdam (2006)
Boeva, V., Ekenberg, L.: A Transition Logic for Schemata Conflicts. Data & Knowledge Engineering 51(3), 277–294 (2004)
Brown, C.E.: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 147–161. Springer, Heidelberg (2011)
Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: EQL-Lite: Effective First-Order Query Processing in Description Logics. In: Veloso, M.M. (ed.) IJCAI 2007, pp. 274–279 (2007)
Fariñas del Cerro, L., Herzig, A., Longin, D., Rifi, O.: Belief Reconstruction in Cooperative Dialogues. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol. 1480, pp. 254–266. Springer, Heidelberg (1998)
Fitting, M.: Types, Tableaus, and Goedel’s God. Kluwer, Amsterdam (2002)
Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer, Amsterdam (1998)
Forbes, G.: Modern Logic. A Text in Elementary Symbolic Logic. OUP, Oxford (1994)
Girle, R.: Modal Logics and Philosophy. Acumen Publ. (2000)
Gödel, K.: An Interpretation of the Intuitionistic Sentential Logic. In: Hintikka, J. (ed.) The Philosophy of Mathematics, pp. 128–129. Oxford University Press, Oxford (1969)
Massacci, F., Donini, F.M.: Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 50–56. Springer, Heidelberg (2000)
Otten, J.: Implementing Connection Calculi for First-order Modal Logics. In: 9th International Workshop on the Implementation of Logics (IWIL 2012), Merida, Venezuela (2012)
Patel-Schneider, P.F., Sebastiani, R.: A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. Journal of Articial Intelligence Research 18, 351–389 (2003)
Popcorn, S.: First Steps in Modal Logic. Cambridge University Press, Cambridge (1994)
Raths, T., Otten, J., Kreitz, C.: The ILTP Problem Library for Intuitionistic Logic. Journal of Automated Reasoning 38(1-3), 261–271 (2007)
Reiter, R.: What Should a Database Know? Journal of Logic Programming 14(1-2), 127–153 (1992)
Sider, T.: Logic for Philosophy. Oxford University Press, Oxford (2009)
Stone, M.: Abductive Planning With Sensing. In: AAAI 1998, Menlo Park, CA, pp. 631–636 (1998)
Stone, M.: Towards a Computational Account of Knowledge, Action and Inference in Instructions. Journal of Language and Computation 1, 231–246 (2000)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)
Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition – CASC-J5. AI Communications 24(1), 75–89 (2011)
Thion, V., Cerrito, S., Cialdea Mayer, M.: A General Theorem Prover for Quantified Modal Logics. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 266–280. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Raths, T., Otten, J. (2012). The QMLTP Problem Library for First-Order Modal Logics. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)