{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:45Z","timestamp":1725663165523},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540116073"},{"type":"electronic","value":"9783540394334"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1982]]},"DOI":"10.1007\/3-540-11607-9_12","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T12:47:54Z","timestamp":1330174074000},"page":"101-108","source":"Crossref","is-referenced-by-count":1,"title":["A theorem-proving approach to the Knuth-Bendix completion algorithm"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Huet G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. Journ. ACM, Vol 27, No 4, October 1980.","DOI":"10.1145\/322217.322230"},{"key":"12_CR2","unstructured":"Huet G.: A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. Rapport de Recherche No 25, INRIA Le Chesnay, 1980."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Huet G., Oppen D.C.: Equations and Rewrite Rules: a Survey. Techn. Report CSL-111, SRI international, January 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"12_CR4","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"Knuth D.E., Bendix P.B.: Simple Word Problems in Universal Algebras. In: \"Computational Problems in Abstract Algebra\", Ed. Leech J., Pergamon, Oxford 1970, pp 263\u2013297."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Loos R.G.K: The Algorithm Description Language ALDES (Report). SIGSAM Bulletin of the ACM, Vol 10 Nr 1, Febr 1976.","DOI":"10.1145\/1093390.1093395"},{"key":"12_CR6","unstructured":"Nilsson N.J.: Problem Solving Methods in Artificial Intelligence. McGraw Hill 1971."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Robinson J.A.: A Machine Oriented Logic Based on the Resolution Principle. Journ. ACM Vol 12 No 1, January 1965.","DOI":"10.1145\/321250.321253"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-11607-9_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:05:11Z","timestamp":1605625511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-11607-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982]]},"ISBN":["9783540116073","9783540394334"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-11607-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1982]]}}}