{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:08Z","timestamp":1747546928815},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540180883"},{"type":"electronic","value":"9783540477471"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-18088-5_6","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:27:55Z","timestamp":1330198075000},"page":"54-71","source":"Crossref","is-referenced-by-count":69,"title":["On word problems in equational theories"],"prefix":"10.1007","author":[{"given":"Jieh","family":"Hsiang","sequence":"first","affiliation":[]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"6_CR1","unstructured":"L. Bachmair, N. Dershowitz and J. Hsiang, Orderings for Equational Proofs, Symposium on Logic in Computer Science, Boston, June 1986."},{"key":"6_CR2","unstructured":"T. Brown, \u201cA Structured Design Method for Specialized Proof Procedures\u201d, Ph.D. Thesis, Cal Tech., 1974."},{"key":"6_CR3","unstructured":"C. L. Chang and C. T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"issue":"3","key":"6_CR4","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz, \u201cOrderings for Term Rewriting Systems\u201d, J.TCS, 17, 3 (1982), 279\u2013301.","journal-title":"J.TCS"},{"key":"6_CR5","unstructured":"R. Forgaard, \u201cA Program for Generating and Analyzing Term Rewriting Systems\u201d, Master's Thesis, MIT Lab. for Computer Science, 1984."},{"key":"6_CR6","unstructured":"L. Fribourg, \u201cSLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting\u201d, Symposium on Logic Programming, Boston, July, 1985, 172\u2013184."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"J. Hsiang, \u201cTwo Results in Term Rewriting Theorem Proving\u201d, Proc. of 1st International Conference in Rewrite Techniques and Applications, Dijon, May, 1985.","DOI":"10.1007\/3-540-15976-2_15"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"J. Hsiang and M. Rusinowitch, \u201cA New Method for Establishing Refutational Completeness in Theorem Proving\u201d, 8th CADE, Oxford, England, 1986, 141\u2013152.","DOI":"10.1007\/3-540-16780-3_86"},{"key":"6_CR9","unstructured":"G. Huet and D. S. Lankford, \u201cOn the Uniform Halting Problem for Term Rewriting Systems\u201d, Report 283, INRIA, 1978."},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G. Huet, \u201cA Complete Proof of Correctness of Knuth-Bendix Completion Algorithm\u201d, J. Computer and System Sciences, 23, (1981), 11\u201321.","journal-title":"J. Computer and System Sciences"},{"key":"6_CR11","unstructured":"J. P. Jouannaud, P. Lescanne and F. Reinig, \u201cRecursive Decomposition Ordering\u201d, Conf. on Formal Description of Programming Concepts II, 1982, 331\u2013346."},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. Jouannaud","year":"1986","unstructured":"J. Jouannaud and H. Kirchner, \u201cCompletion of a Set of Rules Modulo a Set of Equations\u201d, SIAM Journal on Computing, 15, (November 1986), 1155\u20131194.","journal-title":"SIAM Journal on Computing"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix, \u201cSimple Word Problems in Universal Algebras\u201d, in Computational Algebra, J. Leach, (ed.), Pergamon Press, 1970, 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"6_CR14","unstructured":"R. A. Kowalski and P. Hayes, \u201cSemantic Trees in Automatic Theorem Proving\u201d, in Machine Intelligence, vol. 5, B. Meltzer and D. Michie, (eds.), American Elsevier, 1969, 181\u2013201."},{"key":"6_CR15","unstructured":"R. Kowalski, \u201cSearch Strategies for Theorem Proving\u201d, in Machine Intelligence, vol. 5, B. Meltzer and D. Michie, (eds.), American Elsevier, 1970, 181\u2013201."},{"key":"6_CR16","unstructured":"D. S. Lankford, \u201cCanonical Inference\u201d, Report ATP-32, Univ. of Texas at Austin, 1975."},{"key":"6_CR17","unstructured":"D. S. Lankford and A. M. Ballantyne, \u201cDecision Procedure for Simple Equational Theories with Commutative-Associative Axioms\u201d, Report ATP-39, Univ. of TExas at Austin, 1977."},{"key":"6_CR18","unstructured":"J. Mzali, \u201cMethodes de Filtrage Equationnel et de Preuve Automatique de Theoremes\u201d, These de Doctorat de l'Universite de Nancy I, 1986."},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"J. Pedersen, \u201cObtaining Complete Sets of Reductions and Equations without using Special Unification Algorithms\u201d, Unpublished manuscript, 1985.","DOI":"10.1007\/3-540-15984-3_302"},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"G. E. Peterson and M. E. Stickel, \u201cComplete Sets of Reductions for Some Equational Theories\u201d, J. ACM, 28, (1981), 233\u2013264.","journal-title":"J. ACM"},{"key":"6_CR21","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"G. E. Peterson, \u201cA Technique for Establishing Completeness Results in Theorem Proving with Equality\u201d, SIAM J. of Computing, 12, 1 (1983), 82\u2013100.","journal-title":"SIAM J. of Computing"},{"key":"6_CR22","volume-title":"\u201cA Recursively Defined Ordering for Proving Termination of Term Rewriting Systems\u201d, UIUCDCS-R-78-943","author":"D. A. Plaisted","year":"1978","unstructured":"D. A. Plaisted, \u201cA Recursively Defined Ordering for Proving Termination of Term Rewriting Systems\u201d, UIUCDCS-R-78-943, Univ. of Illinois, Urbana, IL, 1978."},{"key":"6_CR23","unstructured":"D. Plaisted, \u201cPrivate Communication\u201d,, 1985."},{"key":"6_CR24","unstructured":"K. Sakai, \u201cKnuth-Bendix Algorithm for Thue System Based on Kachinuki Ordering\u201d, Technical Report, 0087, ICOT, 1985."},{"key":"6_CR25","unstructured":"\u201cAssoc. of Automated Reasoning Newsletter\u201d,, 1985."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-18088-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:12Z","timestamp":1605644052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-18088-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540180883","9783540477471"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-18088-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1987]]}}}