{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:21:35Z","timestamp":1725664895197},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616979"},{"type":"electronic","value":"9783540706359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61697-7_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:13:42Z","timestamp":1330294422000},"page":"63-64","source":"Crossref","is-referenced-by-count":1,"title":["WALDMEISTER: High performance equation theorem proving"],"prefix":"10.1007","author":[{"given":"Arnim","family":"Buch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Fettig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"6_CR1","volume-title":"Collection on the Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair, N. Dershowitz, and D.A. Plaisted. Completion without failure. In Collection on the Resolution of Equations in Algebraic Structures. Academic Press, Austin, 1989."},{"key":"6_CR2","unstructured":"A. Buch and Th. Hillenbrand. Waldmeister: Development of a high performance completion-based theorem prover. SEKI-Report 96-01, Univ. Kaiserslautern, 1996. Available via ftp:\/\/ftp.uni-kl.de\/"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"J. Christian. Fast Knuth-Bendix completion: A summary. In Proc. 3rd RTA, vol. 355 of LNCS, 1989.","DOI":"10.1007\/3-540-51081-8_136"},{"key":"6_CR4","unstructured":"P. Graf. Term Indexing, vol. 1053 of LNAI. Springer Verlag, 1995."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Th. Hillenbrand, A. Buch, and R. Fettig. On gaining efficiency in completion-based theorem proving. In Proc. 7th RTA, LNCS, 1996.","DOI":"10.1007\/3-540-61464-8_74"},{"key":"6_CR6","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra. Computational Problems in Abstract Algebra, 1970."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"E. Lusk and L. Wos. Benchmark problems in which equality plays the major role. In Proc. 11th CADE, vol. 607 of LNCS, 1992.","DOI":"10.1007\/3-540-55602-8_224"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning, 8(3), 1992.","DOI":"10.1023\/A:1005843212881"}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61697-7_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:35:38Z","timestamp":1619573738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61697-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616979","9783540706359"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-61697-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}