{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:56Z","timestamp":1725664796823},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_74","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:40:36Z","timestamp":1330274436000},"page":"432-435","source":"Crossref","is-referenced-by-count":2,"title":["On gaining efficiency in completion-based theorem proving"],"prefix":"10.1007","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":"Fettig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"J. Avenhaus and J. Denzinger. Distributing equational theorem proving. In Proc. 5th RTA, vol. 690 of LNCS, 1993.","DOI":"10.1007\/3-540-56868-9_6"},{"key":"37_CR2","unstructured":"A. Buch and Th. Hillenbrand. Waldmeister: Development of a high performance completion-based theorem prover. SEKI-Report 96-01, Universit\u00e4t Kaiserslautern, 1996."},{"key":"37_CR3","doi-asserted-by":"crossref","unstructured":"J. Christian. Past Knuth-Bendix completion: A summary. In Proc. 3rd RTA, vol. 355 of LNCS, 1989.","DOI":"10.1007\/3-540-51081-8_136"},{"key":"37_CR4","unstructured":"P. Graf. Term Indexing, vol. 1053 of LNAI. Springer Verlag, 1995."},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. 14th ICALP, vol. 267 of LNCS, 1987.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"37_CR6","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebra. Computational Problems in Abstract Algebra, 1970."},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"E. Lusk and R.A. Overbeek. Reasoning about equality. JAR, 2, 1985.","DOI":"10.1007\/BF00244996"},{"key":"37_CR8","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":"37_CR9","doi-asserted-by":"crossref","unstructured":"W. McCune. Experiments with discrimination-tree indexing and path indexing for term retrieval. JAR, 8(3), 1992.","DOI":"10.1007\/BF00245458"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"C.C. Sims. The Knuth-Bendix procedure for strings as a substitute for coset enumeration. JSR, 12, 1991.","DOI":"10.1016\/S0747-7171(08)80096-X"},{"key":"37_CR11","unstructured":"A. Tarski. Logic, Semantics, Metamathematics. Oxford Univ. Press, 1956."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_74.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:06:35Z","timestamp":1605629195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_74"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_74","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}