{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:19:29Z","timestamp":1725761969514},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_9","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"127-136","source":"Crossref","is-referenced-by-count":5,"title":["HOL Based First-Order Modal Logic Provers"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Raths","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Benzm\u00fcller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Proc. of ECAI 2012, Montpellier, France (2012)"},{"key":"9_CR2","unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In: Reasoning in Simple Type Theory: Festschrift in Honour of Peter B. Andrews. Studies in Logic, Mathematical Logic and Foundations, vol.\u00a017, pp. 401\u2013422. College Publications (2008)"},{"issue":"1","key":"9_CR3","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.C.: Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics)\u00a07(1), 7\u201320 (2013)","journal-title":"Logica Universalis (Special Issue on Multimodal Logics)"},{"key":"9_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"9_CR5","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":"J.C. 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.\u00a06172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"9_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"C.E. Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: An automated higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer (1998)","DOI":"10.1007\/978-94-011-5292-1"},{"key":"9_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/10722086_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.: MSPASS: Modal Reasoning by Translation and First-Order Resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol.\u00a01847, pp. 67\u201371. Springer, Heidelberg (2000)"},{"key":"9_CR9","unstructured":"Lindblad, F.: agsyHol (2012), \n                  \n                    https:\/\/github.com\/frelindb\/agsyHOL"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"9_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-71070-7_23","volume-title":"Automated Reasoning","author":"J. Otten","year":"2008","unstructured":"Otten, J.: leancop 2.0 and ileancop 1.2: High performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 283\u2013291. Springer, Heidelberg (2008)"},{"key":"9_CR12","unstructured":"Otten, J.: Implementing connection calculi for first-order modal logics. In: Schulz, S., Ternovska, E., Korovin, K. (eds.) Intl. WS on the Implementation of Logics (2012)"},{"key":"9_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-31365-3_35","volume-title":"Automated Reasoning","author":"T. Raths","year":"2012","unstructured":"Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 454\u2013461. Springer, Heidelberg (2012)"},{"issue":"1-2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T. Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP Problem Library for Intuitionistic Logic - Release v1.1. Journal of Automated Reasoning\u00a038(1-2), 261\u2013271 (2007)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"9_CR16","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. Journal of Formalized Reasoning\u00a03(1), 1\u201327 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"9_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-45616-3_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V. Thion","year":"2002","unstructured":"Thion, V., Cerrito, S., Cialdea Mayer, M.: A general theorem prover for quantified modal logics. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 266\u2013280. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T04:43:00Z","timestamp":1558759380000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}