{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T23:48:59Z","timestamp":1649029739889},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540551249","type":"print"},{"value":"9783540467373","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55124-7_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:48:57Z","timestamp":1330249737000},"page":"197-209","source":"Crossref","is-referenced-by-count":0,"title":["Complete equational unification based on an extension of the Knuth-Bendix completion procedure"],"prefix":"10.1007","author":[{"given":"Akihiko","family":"Ohsuga","sequence":"first","affiliation":[]},{"given":"K\u00f4","family":"Sakai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"8_CR1","unstructured":"Bachmair, L., Dershowitz, N., and Hsiang, J.: Ordering for equational proof, Proc. Symp. Logic in Computer Science, Cambridge, Massachusetts (June 1986)"},{"key":"8_CR2","unstructured":"Bachmair, L., Dershowitz, N., and Plaisted, D. A.: Completion without failure, Proc. Colloquium on Resolution of Equations in Algebraic Structures (1987)"},{"key":"8_CR3","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/BFb0014986","volume":"250","author":"P. G. Bosco","year":"1987","unstructured":"Bosco, P. G., Giovannetti, F., and Moiso, C.: Refined strategies for equational proofs, TAPSOFT '87, LNCS 250, pp. 276\u2013290 (1987)","journal-title":"TAPSOFT '87, LNCS"},{"key":"8_CR4","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N. and Manna, Z.: Proving termination with multiset orderings, Comm. ACM 22, pp. 465\u2013467 (1979)","journal-title":"Comm. ACM"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems, Theoretical Computer Science 17, pp. 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"8_CR6","first-page":"194","volume":"170","author":"F. Fages","year":"1984","unstructured":"Fages, F.: Associative-commutative unification, 7th International Conference on Automated Deduction, LNCS 170, pp. 194\u2013208 (1984)","journal-title":"7th International Conference on Automated Deduction, LNCS"},{"key":"8_CR7","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0304-3975(86)90175-1","volume":"43","author":"F. Fages","year":"1986","unstructured":"Fages, F. and Huet, G.: Complete sets of unifiers and matchers in equational theories, Theoretical Computer Science 43, pp. 189\u2013200 (1986)","journal-title":"Theoretical Computer Science"},{"key":"8_CR8","unstructured":"Fay, M.: First order unification in an equational theory, 4th workshop on Automated Deduction, Austin, Texas, pp. 161\u2013167 (1979)"},{"key":"8_CR9","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/3-540-17220-3_19","volume":"256","author":"J. H. Gallier","year":"1987","unstructured":"Gallier, J. H. and Snyder, W.: A general complete E-unification procedure, Rewriting Techniques and Applications, LNCS 256, pp. 216\u2013227 (1987)","journal-title":"Rewriting Techniques and Applications, LNCS"},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0747-7171(87)80024-X","volume":"3","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J.: Rewrite method for theorem proving in first order theory with equality, J. Symbolic Computation, 3, 133\u2013151 (1987)","journal-title":"J. Symbolic Computation"},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0020-0190(78)90078-9","volume":"7","author":"G. Huet","year":"1978","unstructured":"Huet, G.: An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations, Inform. Process. Lett. 7, pp. 144\u2013147 (1978)","journal-title":"Inform. Process. Lett."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Huet, G. and Oppen, D. C.: Equations and Rewrite Rules: a survey, Formal Language: Perspectives and Open Problems Academic Press, pp. 349\u2013405 (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G.: A complete proof of correctness of the Knuth-Bendix completion algorithm, J. Computer and System Science 23, pp. 11\u201321 (1981)","journal-title":"J. Computer and System Science"},{"key":"8_CR14","first-page":"318","volume":"87","author":"J. M. Hullot","year":"1980","unstructured":"Hullot, J. M.: Canonical forms and unification, 5th Workshop on Automated Deduction, LNCS 87, pp. 318\u2013334 (1980)","journal-title":"5th Workshop on Automated Deduction, LNCS"},{"key":"8_CR15","volume-title":"Computational problems in abstract algebra","author":"D. E. Knuth","year":"1970","unstructured":"Knuth, D. E. and Bendix, P. B.: Simple word problems in universal algebras, Computational problems in abstract algebra, Pergamon Press, Oxford (1970)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Makanin, G. S.: The problem of solvability of equations in a free semigroup, Soviet Akad. Nauk SSSR, Tom 233, No. 2 (1977)","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. ACM 12, pp. 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"8_CR18","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition: an extension of the Knuth and Bendix procedure to acomplete set of inference rules, International Conference on Fifth Generation Computer Systems, 1988, pp. 524\u2013531 (1988)"},{"key":"8_CR19","unstructured":"Sakai, K.: An ordering method for term rewriting systems, Technical Report 062, ICOT (1984)"},{"key":"8_CR20","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. H. Siekmann","year":"1989","unstructured":"Siekmann, J. H.: Unification theory, J. Symbolic Computation 7, pp. 207\u2013274 (1989)","journal-title":"J. Symbolic Computation"},{"key":"8_CR21","unstructured":"Smullyan, R. M.: To Mock a Mockingbird, Alfred A. Knopf, Inc. (1985)"},{"issue":"3","key":"8_CR22","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. E. Stickel","year":"1981","unstructured":"Stickel, M.E.: A unification algorithm for associative-commutative functions, J. ACM, 28, 3, pp. 423\u2013434 (1981)","journal-title":"J. ACM"}],"container-title":["Word Equations and Related Topics","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55124-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:57:45Z","timestamp":1605646665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55124-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551249","9783540467373"],"references-count":22,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-55124-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1992]]}}}