{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:21:16Z","timestamp":1737091276773,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540437925"},{"type":"electronic","value":"9783540480860"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","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":[[2002]]},"DOI":"10.1007\/3-540-48086-2_92","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T06:54:50Z","timestamp":1180335290000},"page":"819-829","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Combining Parallel and Distributed Search in Automated Equational Deduction"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Sinz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Denzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Avenhaus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,6]]},"reference":[{"key":"92_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-52531-9_138","volume-title":"DISCO\u201990","author":"S. Anantharaman","year":"1990","unstructured":"S. Anantharaman and N. Andrianarievelo. Heuristical criteria in refu-tational theorem proving. In DISCO\u201990 (LNCS 429), pages 184\u2013193. Springer-Verlag, 1990."},{"key":"92_CR2","first-page":"1","volume":"1","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion without failure. In Rewriting Techniques, chapter 1, pages 1\u201330. Academic Press, 1989.","journal-title":"Rewriting Techniques"},{"key":"92_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-59200-8_74","volume-title":"Rewriting Techniques and Applications","author":"R. B\u00fcndgen","year":"1995","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. Parallel ReDuX \u2192 PaReDuX. In Rewriting Techniques and Applications (LNCS 914), pages 408\u2013413, 1995."},{"key":"92_CR4","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, W. K\u00fcchlin, and A. Weber. Parallel term rewriting with PaReDuX. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction\u2014A Basis for Applications, Volume II: Systems and Implementation Techniques, volume 9 of Applied Logic Series, pages 231\u2013260. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_9"},{"issue":"1","key":"92_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00881910","volume":"13","author":"M. P. Bonacina","year":"1994","unstructured":"M. P. Bonacina and J. Hsiang. Parallelization of deduction strategies: An analytical study. J. Automated Reasoning, 13(1):1\u201333, 1994.","journal-title":"J. Automated Reasoning"},{"key":"92_CR6","doi-asserted-by":"crossref","unstructured":"J. Denzinger and M. Fuchs. Goal-oriented equational theorem proving using teamwork. In KI-94 (LNAI 861), pages 343\u2013354, 1994.","DOI":"10.1007\/3-540-58467-6_30"},{"key":"92_CR7","doi-asserted-by":"crossref","unstructured":"J. Denzinger and M. Fuchs. A comparison of equality reasoning heuristics. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction\u2014 A Basis for Applications, Volume II: Systems and Implementation Techniques, volume 9 of Applied Logic Series, pages 361\u2013382. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_13"},{"key":"92_CR8","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Formal Models and Semantics, volume 2 of Handbook of Theoretical Computer Science. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"2","key":"92_CR9","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J. Denzinger","year":"1997","unstructured":"J. Denzinger, M. Kronenburg, and S. Schulz. DISCOUNT-a distributed and learning equational prover. J. Automated Reasoning, 18(2):189\u2013198, 1997.","journal-title":"J. Automated Reasoning"},{"key":"92_CR10","unstructured":"J. Denzinger and J. Lind. TWlib\u2014a library for distributed search applications. In Proc. ICS\u201996-AI, pages 101\u2013108, 1996."},{"key":"92_CR11","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G. Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comput. Syst. Sci., 23:11\u201321, 1981.","journal-title":"J. Comput. Syst. Sci."},{"key":"92_CR12","unstructured":"D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra. Pergamon Press, 1970."},{"key":"92_CR13","doi-asserted-by":"crossref","unstructured":"W. K\u00fcchlin and J. A. Ward. Experiments with virtual C Threads. In SPDP\u201992, pages 50\u201355. IEEE Press, 1992.","DOI":"10.1109\/SPDP.1992.242764"},{"key":"92_CR14","volume-title":"Technical Report 95-06","author":"P. Maier","year":"1995","unstructured":"P. Maier, M. G\u00f6bel, and R. B\u00fcndgen. A multi-threaded unfailing completion. Technical Report 95-06, WSI, Universit\u00e4t T\u00fcbingen, Germany, 1995."},{"key":"92_CR15","unstructured":"C. B. Suttner and J. Schumann. Parallel automated theorem proving. In Parallel Processing for Artificial Intellegence PPAI-93. Elsevier, Amsterdam, 1993."},{"issue":"2","key":"92_CR16","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"G. Sutcliffe and C. Suttner. The TPTP problem library-CNF release v1.2.1. J. Automated Reasoning, 21(2):177\u2013203, 1998.","journal-title":"J. Automated Reasoning"},{"key":"92_CR17","doi-asserted-by":"crossref","unstructured":"A. Tarski and S. Givant. A Formalization of Set Theory without Variables, volume 41 of Colloquium Publications. American Mathematical Society, 1987.","DOI":"10.1090\/coll\/041"}],"container-title":["Lecture Notes in Computer Science","Parallel Processing and Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48086-2_92","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T18:36:46Z","timestamp":1737052606000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48086-2_92"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540437925","9783540480860"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48086-2_92","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"6 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}