{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:38Z","timestamp":1725573098794},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_27","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"415-431","source":"Crossref","is-referenced-by-count":4,"title":["Can a Higher-Order and a First-Order Theorem Prover Cooperate?"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]},{"given":"Mateja","family":"Jamnik","sequence":"additional","affiliation":[]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to mathematical logic and Type Theory: To Truth through Proof","author":"P. Andrews","year":"2002","unstructured":"Andrews, P.: An Introduction to mathematical logic and Type Theory: To Truth through Proof. Applied Logic Series, vol.\u00a027. Kluwer, Dordrecht (2002)"},{"key":"27_CR2","unstructured":"Benzm\u00fcller, C.: Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Universit\u00e4t des Saarlandes, Germany (1999)"},{"key":"27_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-48660-7_39","volume-title":"Automated Deduction - CADE-16","author":"C. Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 399\u2013413. Springer, Heidelberg (1999)"},{"issue":"1-2","key":"27_CR4","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1020840027781","volume":"133","author":"C. Benzm\u00fcller","year":"2002","unstructured":"Benzm\u00fcller, C.: Comparing approaches to resolution based higher-order theorem proving. Synthese\u00a0133(1-2), 203\u2013235 (2002)","journal-title":"Synthese"},{"key":"27_CR5","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., Jamnik, M., Kerber, M., Sorge, V.: 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":"27_CR6","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, p. 139. Springer, Heidelberg (1998)"},{"key":"27_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0057438","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"C. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Sorge, V.: A Blackboard Architecture for Guiding Interactive Proofs. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol.\u00a01480, pp. 102\u2013114. Springer, Heidelberg (1998)"},{"key":"27_CR8","unstructured":"Benzm\u00fcller, C., Sorge, V.: Oants \u2013 An open approach at combining Interactive and Automated Theorem Proving. In: Proc. of Calculemus-2000, AK Peters (2001)"},{"key":"27_CR9","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.: Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, p. 365. Springer, Heidelberg (1998)"},{"key":"27_CR10","unstructured":"Brown, C.E.: Set Comprehension in Church\u2019s Type Theory. PhD thesis, Dept. of Mathematical Sciences, Carnegie Mellon University, USA (2004)"},{"key":"27_CR11","unstructured":"de Nivelle, H.: The Bliksem Theorem Prover, Version 1.12. Max-Planck-Institut, Saarbr\u00fccken, Germany (1999), \n                  \n                    http:\/\/www.mpi-sb.mpg.de\/bliksem\/manual.ps"},{"key":"27_CR12","first-page":"10","volume-title":"Proc. IJCAI-16","author":"J. Denzinger","year":"1999","unstructured":"Denzinger, J., Fuchs, D.: Cooperation of Heterogeneous Provers. In: Proc. IJCAI-16, pp. 10\u201315. Morgan Kaufmann, San Francisco (1999)"},{"key":"27_CR13","unstructured":"Fisher, M., Ireland, A.: Multi-agent proof-planning. In: CADE-15 Workshop \u201cUsing AI methods in Deduction\u201d (1998)"},{"key":"27_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-45085-6_31","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 335\u2013349. Springer, Heidelberg (2003)"},{"key":"27_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-45620-1_10","volume-title":"Automated Deduction - CADE-18","author":"J. Hurd","year":"2002","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 134\u2013138. Springer, Heidelberg (2002)"},{"key":"27_CR16","unstructured":"Kerber, M.: On the Representation of Mathematical Concepts and their Translation into First Order Logic. PhD thesis, Universit\u00e4t Kaiserslautern, Germany (1992)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721959_37","volume-title":"Automated Deduction - CADE-17","author":"A. Meier","year":"2000","unstructured":"Meier, A.: TRAMP: Transformation ofMachine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, Springer, Heidelberg (2000)"},{"key":"27_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-25984-8_28","volume-title":"Automated Reasoning","author":"J. Meng","year":"2004","unstructured":"Meng, J., Paulson, L.C.: Experiments on supporting interactive proof using resolution. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 372\u2013384. Springer, Heidelberg (2004)"},{"key":"27_CR19","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":"27_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1007\/3-540-45744-5_56","volume-title":"Automated Reasoning","author":"D. Pastre","year":"2001","unstructured":"Pastre, D.: Muscadet2.3: A knowledge-based theorem prover based on natural deduction. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 685\u2013689. Springer, Heidelberg (2001)"},{"key":"27_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"key":"27_CR22","unstructured":"Sorge, V.: OANTS: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Universit\u00e4t des Saarlandes, Germany (2001)"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/10722086_34","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"G. Stenz","year":"2000","unstructured":"Stenz, G., Wolf, A.: E-SETHEO: An Automated3 Theorem Prover \u2013 System Abstract. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 436\u2013440. Springer, Heidelberg (2000)"},{"issue":"2","key":"27_CR24","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"}],"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-540-32275-7_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:46:57Z","timestamp":1620013617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}