{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:11:35Z","timestamp":1761621095790},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_76","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:58:38Z","timestamp":1330196318000},"page":"5-20","source":"Crossref","is-referenced-by-count":48,"title":["Commutation, transformation, and termination"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[]},{"given":"Nachum","family":"Dershowitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., and Plaisted, D.A. (1985). Termination orderings for associative-commutative rewriting systems, J. of Symbolic Computation 1, 329\u2013349.","journal-title":"J. of Symbolic Computation"},{"key":"2_CR2","unstructured":"Ben Cherifa, A., and Lescanne, P. (1985). A method for proving termination of rewriting systems based on elementary computations on polynomials, unpublished manuscript."},{"key":"2_CR3","series-title":"Lect. Notes in Comp. Science","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1007\/3-540-10843-2_36","volume-title":"Proc. 8th EATCS Int. Colloquium on Automata, Languages and Programming","author":"N. Dershowitz","year":"1981","unstructured":"Dershowitz, N. (1981). Termination of linear rewriting systems, Proc. 8th EATCS Int. Colloquium on Automata, Languages and Programming, S. Even and O. Kariv, eds., Lect. Notes in Comp. Science 115, New York, Springer, 448\u2013458."},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N. (1982). Orderings for term-rewriting systems, Theoretical Computer Science 17, 279\u2013301.","journal-title":"Theoretical Computer Science"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","volume":"64","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N. (1985a). Computing with rewrite systems, Information and Control 64, 122\u2013157.","journal-title":"Information and Control"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. (1985b). Termination. Proc. 1st Int. Conf. on Rewriting Techniques and Applications, Dijon, France, Lect. Notes in Comp. Science, Springer, 180\u2013224.","DOI":"10.1007\/3-540-15976-2_9"},{"key":"2_CR7","unstructured":"Dershowitz, N., Hsiang, J., Josephson, N.A., and Plaisted, D.A. (1984). Associative-commutative rewtiting. Proc. 8th IJCAI, Karlsruhe, 940\u2013944."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1137\/0212012","volume":"12","author":"J.V. Guttag","year":"1983","unstructured":"Guttag, J.V., Kapur, D., and Musser, D.R. (1983). On proving uniform termination and restricted termination of rewriting systems. SIAM Computing 12, 189\u2013214.","journal-title":"SIAM Computing"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Hsiang, J. (1985). Refutational theorem proving using term-rewriting systems. Artificial Intelligence 25, 255\u2013300.","journal-title":"Artificial Intelligence"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G. (1980). Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27, 797\u2013821.","journal-title":"J. ACM"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G. and Hullot, J.M. (1982). Proofs by induction in equational theories with constructors. J. of Comp. and System Sciences 25, 239\u2013266.","journal-title":"J. of Comp. and System Sciences"},{"key":"2_CR12","series-title":"Lect. Notes in Comp. Science","first-page":"175","volume-title":"Proc. 7th Int. Conf. on Automated Deduction","author":"J.-P. Jouannaud","year":"1984","unstructured":"Jouannaud, J.-P., and Munoz, M. (1984). Termination of a set of rules modulo a set of equations, Proc. 7th Int. Conf. on Automated Deduction, R. Shostak, ed., Lect. Notes in Comp. Science 170, Berlin, Springer, 175\u2013193."},{"key":"2_CR13","unstructured":"Kamin, S., and Levy, J.J. (1980). Two generalizations of the recursive path ordering. Unpublished manuscript, Univ. of Illinois at Urbana-Champaign."},{"key":"2_CR14","unstructured":"Kapur, D., and Sivakumar, G. (1984). Architecture of and experiments with RRL, a rewrite rule laboratory. Proc. NSF Workshop on the Rewrite Rule Laboratory, Rensellaerville, New York, 33\u201356."},{"key":"2_CR15","volume-title":"On proving term rewriting systems are noetherian. Memo MTP-3","author":"D.S. Lankford","year":"1979","unstructured":"Lankford, D.S. (1979). On proving term rewriting systems are noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. Univ., Ruston, Louisiana."},{"key":"2_CR16","unstructured":"Manna, Z., and Ness, S. (1970). On the termination of Markov algorithms. Proc. Third Hawaii Int. Conf. on System Science, 789\u2013792."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Musser, D.R. (1980). On proving inductive properties of abstract data types. Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, 154\u2013162.","DOI":"10.1145\/567446.567461"},{"key":"2_CR18","volume-title":"Equational logic as a programming language","author":"M.J. O'Donnell","year":"1985","unstructured":"O'Donnell, M.J. (1985). Equational logic as a programming language. MIT Press, Cambridge, Massachusetts."},{"key":"2_CR19","unstructured":"Plaisted, D.A. (1984). Associative path orderings, Proc. NSF Workshop on the Rewrite Rule Laboratory, Rensellaerville, New York, 123\u2013126."},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1145\/322217.322229","volume":"27","author":"J.C. Raoult","year":"1980","unstructured":"Raoult, J.C., and Vuillemin, J. (1980). Operational and semantic equivalence between recursive programs, J. ACM 27, 772\u2013796.","journal-title":"J. ACM"},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B. Rosen","year":"1973","unstructured":"Rosen, B. (1973). Tree-manipulating systems and Church-Rosser theorems, J. ACM 20, 160\u2013187.","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_76.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:11:40Z","timestamp":1605643900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_76"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_76","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}