{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:43Z","timestamp":1760202523436},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052374","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T05:31:11Z","timestamp":1149658271000},"page":"241-255","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Termination of associative-commutative rewriting by dependency pairs"],"prefix":"10.1007","author":[{"given":"Claude","family":"March\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Urbain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"19_CR1","unstructured":"T. Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Universiteit Utrecht, 1997."},{"key":"19_CR2","volume-title":"Theory and Practice of So\u00dfware Development, volume 1214 of Lecture Notes in Computer Science","author":"T. Arts","year":"1997","unstructured":"T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In M. Bidoit and M. Dauchet, editors, Theory and Practice of So\u00dfware Development, volume 1214 of Lecture Notes in Computer Science, Lille, France, Apr. 1997. Springer-Verlag."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Associative-commutative reduction orderings. Info Proc. Letters, 1992.","DOI":"10.1016\/0020-0190(92)90024-P"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair and N. Dershowitz. Commutation, transformation, and termination. In J. H. Siekmann, editor, Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, pages 5\u201320, July 1986.","DOI":"10.1007\/3-540-16780-3_76"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1\u201318, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR6","unstructured":"L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346\u2013357, June 1986."},{"issue":"4","key":"19_CR7","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"L. Bachmair and D. A. Plaisted. Termination orderings for associativecommutative rewriting systems. Journal of Symbolic Computation, 1(4):329\u2013349, Dec. 1985.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"A. Ben Cherifa and P. Lescanne. An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations. In Proc. 8th Int. Conf. on Automated Deduction, Oxford, England, LNCS 230, pages 42\u201351. Springer-Verlag, July 1986.","DOI":"10.1007\/3-540-16780-3_78"},{"volume-title":"8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science","year":"1997","key":"19_CR9","unstructured":"H. Comon, editor. 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, Barcelona, Spain, June 1997. Springer-Verlag."},{"key":"19_CR10","first-page":"416","volume-title":"7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science","author":"E. Contejean","year":"1996","unstructured":"E. Contejean and C. March\u00e9. CiME: Completion Modulo E. In H. Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416\u2013419, New Brunswick, NJ, USA, July 1996. Springer-Verlag. System Description available at http: \/\/www.lri. fr\/~demons\/cime. html."},{"key":"19_CR11","unstructured":"E. Contejean, C. March\u00e9, and L. Rabehasaina. Rewrite systems for natural, integral, and rational arithmetic. In Comon [9]."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"C. Delor and L. Puel. Extension of the associative path ordering to a chain of associative-commutative symbols. In Proc. 5th Rewriting Techniques and Applications, Montr\u00e9al, LNCS 690, pages 389\u2013404, 1993.","DOI":"10.1007\/3-540-56868-9_29"},{"issue":"3","key":"19_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, Mar. 1982.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69\u2013115, Feb. 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR15","volume-title":"6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science","author":"J. Giesl","year":"1995","unstructured":"J. Giesl. Generating polynomial orderings for termination proofs. In J. Hsiang, editor, 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, Kaiserslautern, Germany, Apr. 1995. Springer-Verlag."},{"key":"19_CR16","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. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comput. Syst. Sci., 23:11\u201321, 1981.","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"19_CR17","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155\u20131194, 1986.","journal-title":"SIAM Journal on Computing"},{"key":"19_CR18","unstructured":"D. Kapur and G. Sivakumar. A total, ground path ordering for proving termination of AC-rewrite systems. In Comon [9]."},{"key":"19_CR19","unstructured":"D. E. Knuth. The art of computer programming, volume 2. Addison-Wesley, 2nd edition, 1981."},{"key":"19_CR20","volume-title":"Proc. 9th CAAP","author":"P. Lescanne","year":"1984","unstructured":"P. Lescanne. Uniform termination of term rewriting systems with status. In Proc. 9th CAAP, Cambridge, 1984. Cambridge University Press."},{"key":"19_CR21","volume-title":"Th\u00e8se de doctorat","author":"C. March\u00e9","year":"1993","unstructured":"C. March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 des probl\u00e8mes du mot dans certaines classes de th\u00e9ories \u00e9quationnelles. Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud, Orsay, France, Oct. 1993."},{"issue":"3","key":"19_CR22","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1006\/jsco.1996.0011","volume":"21","author":"C. March\u00e9","year":"1996","unstructured":"C. March\u00e9. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253\u2013288, 1996.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR23","unstructured":"R. Nieuwenhuis and A. Rubio. A precedence-based total AC-compatible ordering. In C. Kirchner, editor, Proc. 5th Rewriting Techniques and Applications, Montr\u00e9al, LNCS 690. Springer-Verlag, June 1993."},{"issue":"2","key":"19_CR24","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. Complete sets of reductions for some equational theories. J. ACM, 28(2):233\u2013264, Apr. 1981.","journal-title":"J. ACM"},{"key":"19_CR25","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/3-540-56287-7_105","volume-title":"Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science","author":"J. Steinbach","year":"1992","unstructured":"J. Steinbach. Proving polynomials positive. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 191\u2013202, New Delhi, India, Dec. 1992. Springer-Verlag."},{"key":"19_CR26","volume-title":"Rapport de DEA","author":"X. Urbain","year":"1997","unstructured":"X. Urbain. Preuves de terminaison \u00e0 l'aide de paires de d\u00e9pendances. Rapport de DEA, Universit\u00e9 Paris-Sud, Orsay, France, 1997."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:13:54Z","timestamp":1558271634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0052374","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}