{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:27Z","timestamp":1725518427880},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71070-7_14","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T05:56:30Z","timestamp":1219989390000},"page":"162-170","source":"Crossref","is-referenced-by-count":42,"title":["LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Theiss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Fietzke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"P.B. Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.E.: TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic\u00a04(4), 367\u2013395 (2006)","journal-title":"J. Applied Logic"},{"issue":"4","key":"14_CR2","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/s10817-006-9036-z","volume":"36","author":"M. Beeson","year":"2006","unstructured":"Beeson, M.: Mathematical induction in Otter-Lambda. J. Autom. Reasoning\u00a036(4), 311\u2013344 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR3","unstructured":"Benzm\u00fcller, C.: Equality and Extensionality in Automated Higher-Order Theorem Proving. PhD thesis, Saarlandes University (1999)"},{"key":"14_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction - CADE-15","author":"C. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO \u2013 a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 139\u2013143. Springer, Heidelberg (1998)"},{"key":"14_CR5","unstructured":"Benzm\u00fcller, C., Paulson, L.: Festschrift in Honour of Peter B. Andrews on his 70th Birthday. In: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. IFCoLog (to appear, 2007)"},{"key":"14_CR6","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: Progress report on LEO-II \u2013 an automatic theorem prover for higher-order logic. In: TPHOLs 2007 Emerging Trends Proc., Internal Report 364\/07, Department of Computer Science, University Kaiserslautern, Germany, pp. 33\u201348 (2007)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Proc (IJCAR 2008)","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0 \u2014 the core TPTP language for classical higher-order logic. In: Proc (IJCAR 2008). LNCS, vol.\u00a05195. Springer, Heidelberg (2008)"},{"key":"14_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-45422-5_29","volume-title":"KI 2001: Advances in Artificial Intelligence","author":"C. Benzm\u00fcller","year":"2001","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Experiments with an Agent-Oriented Reasoning System. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol.\u00a02174, pp. 409\u2013424. Springer, Heidelberg (2001)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Applied Logic (in print) (2008)","DOI":"10.1016\/j.jal.2007.06.003"},{"key":"14_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/BFb0054272","volume-title":"Automated Deduction - CADE-15","author":"M. Bishop","year":"1998","unstructured":"Bishop, M., Andrews, P.B.: Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 365\u2013380. Springer, Heidelberg (1998)"},{"key":"14_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-45620-1_33","volume-title":"Automated Deduction - CADE-18","author":"C.E. Brown","year":"2002","unstructured":"Brown, C.E.: Solving for Set Variables in Higher-Order Theorem Proving. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 408\u2013422. Springer, Heidelberg (2002)"},{"issue":"5","key":"14_CR12","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math.\u00a034(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"14_CR13","volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","author":"M.J. Gordon","year":"1993","unstructured":"Gordon, M.J., Melham, T.F.: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"14_CR14","unstructured":"Kerber, M.: On the Representation of Mathematical Concepts and their Translation into First-Order Logic. PhD thesis, Univ. Kaiserslautern, Germany (1992)"},{"key":"14_CR15","unstructured":"Klein, L.: Indexing f\u00fcr Terme h\u00f6herer Stufe. Master\u2019s thesis, Saarland Univ. (1997)"},{"issue":"2","key":"14_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Automated Reasoning\u00a09(2), 147\u2013167 (1992)","journal-title":"J. Automated Reasoning"},{"key":"14_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-45744-5_19","volume-title":"Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 257\u2013271. Springer, Heidelberg (2001)"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/978-3-540-24599-5_26","volume-title":"Logic Programming","author":"B. Pientka","year":"2003","unstructured":"Pientka, B.: Higher-order substitution tree indexing. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol.\u00a02916, pp. 377\u2013391. Springer, Heidelberg (2003)"},{"issue":"2-3","key":"14_CR20","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AICOM\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AICOM"},{"issue":"2\/3","key":"14_CR21","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. J. AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"J. AI Communications"},{"issue":"4","key":"14_CR22","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J. Siekmann","year":"2006","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with OMEGA. J. Applied Logic\u00a04(4), 533\u2013559 (2006)","journal-title":"J. Applied Logic"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Stickel, M.: The path-indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, USA (1989)","DOI":"10.21236\/ADA460990"},{"key":"14_CR24","unstructured":"Theiss, F., Benzm\u00fcller, C.: Term indexing for the LEO-II prover. In: Proc. of the 6th International Workshop on the Implementation of Logics. CEUR Workshop Proc., vol.\u00a0212 (2006)"},{"key":"14_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., et al.: Spass version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T11:35:31Z","timestamp":1558265731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710691","9783540710707"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}