{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:10:49Z","timestamp":1761621049720},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_27","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"317-321","source":"Crossref","is-referenced-by-count":5,"title":["The New WALDMEISTER Loop at Work"],"prefix":"10.1007","author":[{"given":"Jean-Marie","family":"Gaillourdet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"L\u00f6chner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Spies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: Resolution of Equations in Algebraic Structures, vol.\u00a02, pp. 1\u201330. Academic Press, London (1989)"},{"key":"27_CR2","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-94-017-0435-9_9","volume-title":"Automated Deduction\u2014A Basis for Applications: Systems and Implementation Techniques","author":"R. B\u00fcndgen","year":"1998","unstructured":"B\u00fcndgen, R., G\u00f6bel, M., K\u00fcchlin, W., Weber, A.: Parallel term rewriting with PaReDuX. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction\u2014A Basis for Applications: Systems and Implementation Techniques, vol.\u00a0II, pp. 231\u2013260. Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"1\u20134","key":"27_CR3","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1023\/A:1018932114059","volume":"29","author":"M.P. Bonacina","year":"2000","unstructured":"Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence\u00a029(1\u20134), 223\u2013257 (2000)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"27_CR4","first-page":"10","volume-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence","author":"J. Denzinger","year":"1999","unstructured":"Denzinger, J., Fuchs, D.: Cooperation of heterogeneous provers. In: Dean, T. (ed.) Proceedings of the 16th International Joint Conference on Artificial Intelligence, pp. 10\u201315. Morgan Kaufmann, San Francisco (1999)"},{"key":"27_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/3-540-45620-1_38","volume-title":"Automated Deduction - CADE-18","author":"T. Hillenbrand","year":"2002","unstructured":"Hillenbrand, T., L\u00f6chner, B.: The next Waldmeister loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 486\u2013500. Springer, Heidelberg (2002)"},{"issue":"2,3","key":"27_CR6","first-page":"127","volume":"15","author":"B. L\u00f6chner","year":"2002","unstructured":"L\u00f6chner, B., Hillenbrand, T.: A phytography of Waldmeister. AI Communications\u00a015(2,3), 127\u2013133 (2002)","journal-title":"AI Communications"},{"key":"27_CR7","first-page":"71","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"W. McCune","year":"1997","unstructured":"McCune, W.: 33 basic test problems: a practical evaluation of some paramodulation strategies. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, pp. 71\u2013114. MIT Press, Cambridge (1997)"},{"key":"27_CR8","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Tech. Report CSPP-7, University of Manchester (2000)"},{"key":"27_CR9","unstructured":"Suttner, C.B., Sutcliffe, G.: The TPTP problem library (TPTP v2.2.0). Tech. Report 99\/02, James Cook University, Townsville (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T22:01:50Z","timestamp":1553205710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}