{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:36Z","timestamp":1761611076612,"version":"3.41.0"},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1997,4]]},"DOI":"10.1023\/a:1005872405899","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"265-270","source":"Crossref","is-referenced-by-count":33,"title":["WALDMEISTER - High-Performance Equational Deduction"],"prefix":"10.1007","volume":"18","author":[{"given":"Thomas","family":"Hillenbrand","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnim","family":"Buch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Vogt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"L\u00f6chner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"133485_CR1","doi-asserted-by":"crossref","unstructured":"Avenhaus, J., Denzinger, J. and Fuchs, M.: DISCOUNT: A system for distributed equational deduction, in Proc. 6th RTA, LNCS 914, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59200-8_72"},{"key":"133485_CR2","unstructured":"Bachmair, L., Dershowitz, N. and Plaisted, D. A.: Completion without failure, in Coll. on the Resolution of Equations in Algebraic Structures, Academic Press, 1989."},{"key":"133485_CR3","unstructured":"Buch, A. and Hillenbrand, Th.: WALDMEISTER: Development of a High Performance Completion-based Theorem Prover. SEKI-Report 96-01, Univ. Kaiserslautern, 1996."},{"key":"133485_CR4","doi-asserted-by":"crossref","unstructured":"Christian, J.: Fast Knuth-Bendix completion: A summary, in Proc. 3rd RTA, LNCS 355, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_136"},{"key":"133485_CR5","unstructured":"Denzinger, J. and Schulz, S.: Recording, analyzing and presenting distributed deduction processes, in Proc. 1st PASCO, LNSC 5, World Scientific Publishing, 1994."},{"key":"133485_CR6","doi-asserted-by":"crossref","unstructured":"Graf, P.: Term Indexing, LNAI 1053, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61040-5"},{"key":"133485_CR7","doi-asserted-by":"crossref","unstructured":"Lusk, E. and Wos, L.: Benchmark problems in which equality plays the major role, in Proc. 11th CADE, LNCS 607, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_224"},{"issue":"2","key":"133485_CR8","doi-asserted-by":"crossref","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, Journal of Automated Reasoning\n9(2) (1992), 147\u2013167.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005872405899.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005872405899\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005872405899.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:57Z","timestamp":1749123657000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005872405899"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["133485"],"URL":"https:\/\/doi.org\/10.1023\/a:1005872405899","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,4]]}}}