{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T14:40:09Z","timestamp":1751812809969,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999050"},{"type":"electronic","value":"9783319999067"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99906-7_19","type":"book-chapter","created":{"date-parts":[[2018,8,23]],"date-time":"2018-08-23T10:45:38Z","timestamp":1535021138000},"page":"274-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The MET: The Art of Flexible Reasoning with Modalities"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Glei\u00dfner","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Steen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,24]]},"reference":[{"issue":"2,3","key":"19_CR1","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. AI Commun. 15(2,3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: An automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"19_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNAI, vol. 10900, pp. 108\u2013116. Springer, Heidelberg (2018)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"19_CR6","volume-title":"Handbook of Modal Logic","author":"P Blackburn","year":"2006","unstructured":"Blackburn, P., van Benthem, J.F., Wolter, F.: Handbook of Modal Logic, vol. 3. Elsevier, Amsterdam (2006)"},{"unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: The inconsistency in G\u00f6del\u2019s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016, vol. 1\u20133, pp. 936\u2013942. AAAI Press (2016). (Acceptance rate $$\\le 25\\%$$)","key":"19_CR7"},{"issue":"1","key":"19_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s11787-017-0160-9","volume":"11","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-H\u00e1jek controversy. Logica Universalis 11(1), 139\u2013151 (2017)","journal-title":"Logica Universalis"},{"unstructured":"Fuenmayor, D., Benzm\u00fcller, C.: Types, Tableaus and G\u00f6del\u2019s God in Isabelle\/HOL. Archive of Formal Proofs (2017). This publication is machine verified with Isabelle\/HOL, but only mildly human reviewed","key":"19_CR9"},{"issue":"1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Universalis 7(1), 7\u201320 (2013). (Special Issue on Multimodal Logics)","journal-title":"Logica Universalis"},{"issue":"4","key":"19_CR11","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"19_CR12","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1\u201327 (2010)","journal-title":"J. Formaliz. Reason."},{"doi-asserted-by":"crossref","unstructured":"Glei\u00dfner, T., Steen, A., Benzm\u00fcller, C.: Theorem provers for every normal modal logic. In: Eiter, T., Sands, D. (eds.) LPAR-21. EPiC Series in Computing, Maun, Botswana, vol. 46, pp. 14\u201330. EasyChair (2017)","key":"19_CR13","DOI":"10.29007\/jsb9"},{"unstructured":"Andrews, P.: Church\u2019s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Stanford University, Metaphysics Research Lab (2014)","key":"19_CR14"},{"unstructured":"Becker, O.: Zur Logik der Modalit\u00e4ten. Max Niemeyer Verlag (1930)","key":"19_CR15"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"unstructured":"Athan, T., Boley, H., Paschke, A.: Ruleml 1.02: Deliberation, reaction and consumer families. In: Bassiliades, N., et al. (eds.) Proceedings of the RuleML 2015 Challenge, the Special Track on Rule-based Recommender Systems for the Web of Data, the Special Industry Track and the RuleML 2015 Doctoral Consortium hosted by the 9th International Web Rule Symposium (RuleML 2015). CEUR Workshop Proceedings, vol. 1417. CEUR-WS.org (2015)","key":"19_CR17"},{"key":"19_CR18","first-page":"152","volume":"13","author":"ST Cao","year":"2014","unstructured":"Cao, S.T., Nguyen, L.A., Szalas, A.: The web ontology rule language OWL 2 RL$$^{+}$$ and its extensions. Trans. Comput. Collect. Intell. 13, 152\u2013175 (2014)","journal-title":"Trans. Comput. Collect. Intell."},{"unstructured":"Boley, H., Benzm\u00fcller, C., Luan, M., Sha, Z.: Translating higher-order modal logic from RuleML to TPTP. In Giurca, A., et al. (eds.) Proceedings of the RuleML 2016 Challenge, the Special Industry Track and the RuleML 2016 Doctoral Consortium hosted by the 10th International Web Rule Symposium (RuleML 2016). CEUR Workshop Proceedings, vol. 1620. CEUR-WS.org (2016)","key":"19_CR19"}],"container-title":["Lecture Notes in Computer Science","Rules and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99906-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T14:00:44Z","timestamp":1751810444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99906-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999050","9783319999067"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99906-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}