{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:51:10Z","timestamp":1762458670710,"version":"3.41.0"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:p>A termination proof method for rewriting under strategies, based on an explicit induction on the termination property, is presented and instantiated for the innermost, outermost, and local strategies. Rewriting trees are simulated by proof trees generated with an abstraction mechanism, narrowing and constraints representing sets of ground terms. Abstraction introduces variables to represent normal forms without computing them and to control the narrowing mechanism, well known to easily diverge. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. It is established that termination under strategy is equivalent to the construction of finite proof trees schematizing terminating rewriting trees. Sufficient effective conditions to ensure finiteness are studied and the method is illustrated on several examples for each specific strategy.<\/jats:p>","DOI":"10.1145\/1462179.1462182","type":"journal-article","created":{"date-parts":[[2009,2,25]],"date-time":"2009-02-25T14:44:30Z","timestamp":1235573070000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Termination of rewriting under strategies"],"prefix":"10.1145","volume":"10","author":[{"given":"Isabelle","family":"Gnaedig","sequence":"first","affiliation":[{"name":"INRIA and LORIA, Vandoeuvre l\u00e8s Nancy Cedex France"}]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[{"name":"INRIA and LORIA, Vandoeuvre l\u00e8s Nancy Cedex France"}]}],"member":"320","published-online":{"date-parts":[[2009,3,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science","volume":"4337","author":"Alarc\u00f3n B.","unstructured":"Alarc\u00f3n , B. , Guti\u00e9rrez , R. , and Lucas , S . 2006. Context-Sensitive dependency pairs . In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science , vol. 4337 . Springer, 297 --308. Alarc\u00f3n, B., Guti\u00e9rrez, R., and Lucas, S. 2006. Context-Sensitive dependency pairs. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 4337. Springer, 297 --308."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82529-0"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 8th Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science","volume":"1232","author":"Arts T.","unstructured":"Arts , T. and Giesl , J . 1997. Proving innermost normalisation automatically . In Proceedings of the 8th Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science , vol. 1232 . Springer, 157--171. Arts, T. and Giesl, J. 1997. Proving innermost normalisation automatically. In Proceedings of the 8th Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol. 1232. Springer, 157--171."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press New York.   Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press New York.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_2_7_1","volume-title":"Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science","volume":"55","author":"Barendsen E.","unstructured":"Barendsen , E. , Bethke , I. , Heering , J. , Kennaway , R. , Klint , P. , van Oostrom , V. , van Raamsdonk , F. , de Vries , F.-J. , and Zantema , H . 2003 . Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science , vol. 55 . Cambridge University Press. Barendsen, E., Bethke, I., Heering, J., Kennaway, R., Klint, P., van Oostrom, V., van Raamsdonk, F., de Vries, F.-J., and Zantema, H. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90030-X"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Borovansk\u00fd P. Kirchner C. Kirchner H. Moreau P.-E. and Ringeissen C. 1998. An Overview of ELAN. In Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications C. Kirchner and H. Kirchner Eds. Electronic Notes in Theoretical Computer Science. Elsevier Science (North-Holland).  Borovansk\u00fd P. Kirchner C. Kirchner H. Moreau P.-E. and Ringeissen C. 1998. An Overview of ELAN. In Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications C. Kirchner and H. Kirchner Eds. Electronic Notes in Theoretical Computer Science. Elsevier Science (North-Holland).","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"e_1_2_2_10_1","volume-title":"Proceedings of the 17th International Conference on Automated Deduction. Lecture Notes in Computer Science","volume":"1831","author":"Borralleras C.","unstructured":"Borralleras , C. , Ferreira , M. , and Rubio , A . 2000. Complete monotonic semantic path orderings . In Proceedings of the 17th International Conference on Automated Deduction. Lecture Notes in Computer Science , vol. 1831 . Springer, 346--364. Borralleras, C., Ferreira, M., and Rubio, A. 2000. Complete monotonic semantic path orderings. In Proceedings of the 17th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 1831. Springer, 346--364."},{"key":"e_1_2_2_11_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"2027","author":"Brand M.","unstructured":"Brand , M. , Deursen , A. , Heering , J. , Jong , H. , Jonge , M. , Kuipers , T. , Klint , P. , Moonen , L. , Olivier , P. , Scheerder , J. , Vinju , J. , Visser , E. , and Visser , J . 2001. The ASF+SDF meta-environment: A component-based language development environment. In Compiler Construction (CC \u201901), R. Wilhelm , Ed. Lecture Notes in Computer Science , vol. 2027 . Springer, 365--370. Brand, M., Deursen, A., Heering, J., Jong, H., Jonge, M., Kuipers, T., Klint, P., Moonen, L., Olivier, P., Scheerder, J., Vinju, J., Visser, E., and Visser, J. 2001. The ASF+SDF meta-environment: A component-based language development environment. In Compiler Construction (CC \u201901), R. Wilhelm, Ed. Lecture Notes in Computer Science, vol. 2027. Springer, 365--370."},{"key":"e_1_2_2_12_1","first-page":"427","article-title":"The rewriting calculus \u2014 Part I and II","volume":"9","author":"Cirstea H.","year":"2001","unstructured":"Cirstea , H. and Kirchner , C. 2001 . The rewriting calculus \u2014 Part I and II . Logic J. Interest Group Pure App. Logics 9 , 427 -- 498 . Cirstea, H. and Kirchner, C. 2001. The rewriting calculus \u2014 Part I and II. Logic J. Interest Group Pure App. Logics 9, 427--498.","journal-title":"Logic J. Interest Group Pure App. Logics"},{"key":"e_1_2_2_13_1","volume-title":"Electronic Notes in Theoretical Computer Science","volume":"86","author":"Cirstea H.","unstructured":"Cirstea , H. , Kirchner , C. , Liquori , L. , and Wack , B . 2003. Rewrite strategies in the rewriting calculus . In Electronic Notes in Theoretical Computer Science , Vol. 86 , B. Gramlich and S. Lucas, Eds. Elsevier. Cirstea, H., Kirchner, C., Liquori, L., and Wack, B. 2003. Rewrite strategies in the rewriting calculus. In Electronic Notes in Theoretical Computer Science, Vol. 86, B. Gramlich and S. Lucas, Eds. Elsevier."},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 14th International Conference on Rewriting Techniques and Applications, R. Nieuwenhuis, Ed. Lecture Notes in Computer Science","volume":"2706","author":"Clavel M.","unstructured":"Clavel , M. , Dur\u00e1n , F. , Eker , S. , Lincoln , P. , Mart\u00ed-Oliet , N. , Meseguer , J. , and Talcott , C . 2003. The Maude 2.0 system . In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, R. Nieuwenhuis, Ed. Lecture Notes in Computer Science , vol. 2706 . Springer, 76--87. Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., and Talcott, C. 2003. The Maude 2.0 system. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications, R. Nieuwenhuis, Ed. Lecture Notes in Computer Science, vol. 2706. Springer, 76--87."},{"key":"e_1_2_2_15_1","volume-title":"Disunification: A survey. In Computational Logic. Essays in honor of Alan Robinson, J.-L","author":"Comon H.","year":"1991","unstructured":"Comon , H. 1991 . Disunification: A survey. In Computational Logic. Essays in honor of Alan Robinson, J.-L . Lassez and G. Plotkin, Eds. The MIT press , Cambridge, MA , Chapter 9, 322--359. Comon, H. 1991. Disunification: A survey. In Computational Logic. Essays in honor of Alan Robinson, J.-L. Lassez and G. Plotkin, Eds. The MIT press, Cambridge, MA, Chapter 9, 322--359."},{"key":"e_1_2_2_16_1","unstructured":"Comon H. Dauchet M. Gilleron R. Jacquemard F. Lugiez D. Tison S. and Tommasi M. 1997. Tree automata techniques and applications. Release October 1st 2002.  Comon H. Dauchet M. Gilleron R. Jacquemard F. Lugiez D. Tison S. and Tommasi M. 1997. Tree automata techniques and applications. Release October 1st 2002."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00275-4"},{"key":"e_1_2_2_19_1","volume-title":"Rewrite systems, 244--320. Also as Res. rep. 478, LRI.","author":"Dershowitz N.","year":"1990","unstructured":"Dershowitz , N. and Jouannaud , J . -P . 1990 . Handbook of Theoretical Computer Science . Vol. B. Elsevier Science (North-Holland), Chapter 6 : Rewrite systems, 244--320. Also as Res. rep. 478, LRI. Dershowitz, N. and Jouannaud, J.-P. 1990. Handbook of Theoretical Computer Science. Vol. B. Elsevier Science (North-Holland), Chapter 6: Rewrite systems, 244--320. Also as Res. rep. 478, LRI."},{"key":"e_1_2_2_20_1","first-page":"535","article-title":"Rewriting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science","volume":"9","author":"Dershowitz N.","year":"2001","unstructured":"Dershowitz , N. and Plaisted , D. 2001 . Rewriting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science , Chapter 9 , 535 -- 610 . Dershowitz, N. and Plaisted, D. 2001. Rewriting. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. I. Elsevier Science, Chapter 9, 535--610.","journal-title":"Chapter"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80019-2"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the 16th International Conference on Rewriting Techniques and Applications, J. Giesl, Ed. Lecture Notes in Computer Science","volume":"3467","author":"Fern\u00e1ndez M.-L.","unstructured":"Fern\u00e1ndez , M.-L. , Godoy , G. , and Rubio , A . 2005. Orderings for innermost termination . In Proceedings of the 16th International Conference on Rewriting Techniques and Applications, J. Giesl, Ed. Lecture Notes in Computer Science , vol. 3467 . Springer, 17--31. Fern\u00e1ndez, M.-L., Godoy, G., and Rubio, A. 2005. Orderings for innermost termination. In Proceedings of the 16th International Conference on Rewriting Techniques and Applications, J. Giesl, Ed. Lecture Notes in Computer Science, vol. 3467. Springer, 17--31."},{"key":"e_1_2_2_24_1","volume-title":"Selected Papers of the 4th International Workshop on Strategies in Automated Deduction, M. P. Bonacina and B. Gramlich, Eds. Electronic Notes in Theoretical Computer Science","volume":"58","author":"Fissore O.","unstructured":"Fissore , O. , Gnaedig , I. , and Kirchner , H . 2001. Termination of rewriting with local strategies . In Selected Papers of the 4th International Workshop on Strategies in Automated Deduction, M. P. Bonacina and B. Gramlich, Eds. Electronic Notes in Theoretical Computer Science , vol. 58 . Elsevier Science (North-Holland). Fissore, O., Gnaedig, I., and Kirchner, H. 2001. Termination of rewriting with local strategies. In Selected Papers of the 4th International Workshop on Strategies in Automated Deduction, M. P. Bonacina and B. Gramlich, Eds. Electronic Notes in Theoretical Computer Science, vol. 58. Elsevier Science (North-Holland)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571164"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science","volume":"71","author":"Fissore O.","unstructured":"Fissore , O. , Gnaedig , I. , and Kirchner , H . 2002b. Outermost ground termination . In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science , vol. 71 . Elsevier Science (North-Holland). Fissore, O., Gnaedig, I., and Kirchner, H. 2002b. Outermost ground termination. In Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier Science (North-Holland)."},{"key":"e_1_2_2_27_1","unstructured":"Fissore O. Gnaedig I. and Kirchner H. 2002c. Outermost ground termination \u2014 Extended version. Tech. rep. A02-R-493 LORIA Nancy France. December.  Fissore O. Gnaedig I. and Kirchner H. 2002c. Outermost ground termination \u2014 Extended version. Tech. rep. A02-R-493 LORIA Nancy France. December."},{"volume-title":"Proceedings of the 6th International Workshop on Termination, A. Rubio, Ed, 77--79","author":"Fissore O.","key":"e_1_2_2_28_1","unstructured":"Fissore , O. , Gnaedig , I. , and Kirchner , H . 2003a. CARIBOO: A multi-strategy termination proof tool based on induction . In Proceedings of the 6th International Workshop on Termination, A. Rubio, Ed, 77--79 . Fissore, O., Gnaedig, I., and Kirchner, H. 2003a. CARIBOO: A multi-strategy termination proof tool based on induction. In Proceedings of the 6th International Workshop on Termination, A. Rubio, Ed, 77--79."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888264"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science","volume":"3407","author":"Fissore O.","unstructured":"Fissore , O. , Gnaedig , I. , and Kirchner , H . 2004. A proof of weak termination providing the right way to terminate . In Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science , vol. 3407 . Springer, 356--371. Fissore, O., Gnaedig, I., and Kirchner, H. 2004. A proof of weak termination providing the right way to terminate. In Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing. Lecture Notes in Computer Science, vol. 3407. Springer, 356--371."},{"key":"e_1_2_2_31_1","unstructured":"Fissore O. Gnaedig I. Kirchner H. and Moussa L. 2005. Cariboo A termination proof tool for rewriting-based programming languages with strategies version 1.1. Free GPL Licence APP registration IDDN.FR.001.170013.001.S.P.2005.000.10600. Available at http:\/\/cariboo.loria.fr\/.  Fissore O. Gnaedig I. Kirchner H. and Moussa L. 2005. Cariboo A termination proof tool for rewriting-based programming languages with strategies version 1.1. Free GPL Licence APP registration IDDN.FR.001.170013.001.S.P.2005.000.10600. Available at http:\/\/cariboo.loria.fr\/."},{"volume-title":"Proceedings of the 1st IEEE International Conference on Formal Engineering Methods.","author":"Futatsugi K.","key":"e_1_2_2_32_1","unstructured":"Futatsugi , K. and Nakagawa , A . 1997. An overview of the Cafe specification environment -- An algebraic approach for creating, verifying, and maintaining formal specifications over networks . In Proceedings of the 1st IEEE International Conference on Formal Engineering Methods. Futatsugi, K. and Nakagawa, A. 1997. An overview of the Cafe specification environment -- An algebraic approach for creating, verifying, and maintaining formal specifications over networks. In Proceedings of the 1st IEEE International Conference on Formal Engineering Methods."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647197.721002"},{"key":"e_1_2_2_34_1","volume-title":"Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science","volume":"1631","author":"Giesl J.","unstructured":"Giesl , J. and Middeldorp , A . 1999. Transforming context-sensitive rewrite systems . In Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science , vol. 1631 . Springer, 271--285. Giesl, J. and Middeldorp, A. 1999. Transforming context-sensitive rewrite systems. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, vol. 1631. Springer, 271--285."},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the 6th International Conference on Developments in Language Theory (DLT'02)","volume":"2450","author":"Giesl J.","unstructured":"Giesl , J. and Middeldorp , A . 2003. Innermost termination of context-sensitive rewriting . In Proceedings of the 6th International Conference on Developments in Language Theory (DLT'02) . Lecture Notes in Computer Science , vol. 2450 . Springer, 231--244. Giesl, J. and Middeldorp, A. 2003. Innermost termination of context-sensitive rewriting. In Proceedings of the 6th International Conference on Developments in Language Theory (DLT'02). Lecture Notes in Computer Science, vol. 2450. Springer, 231--244."},{"volume-title":"Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 297--312","author":"Giesl J.","key":"e_1_2_2_36_1","unstructured":"Giesl , J. , Swiderski , S. , Schneider-Kamp , P. , and Thiemann , R . 2006. Automated termination analysis for Haskell: From term rewriting to programming languages . In Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 297--312 . Giesl, J., Swiderski, S., Schneider-Kamp, P., and Thiemann, R. 2006. Automated termination analysis for Haskell: From term rewriting to programming languages. In Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 297--312."},{"key":"e_1_2_2_37_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning","author":"Giesl J.","unstructured":"Giesl , J. , Thiemann , R. , and Schneider-Kamp , P. 2004. The dependency pair framework: Combining techniques for automated termination proofs . In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning . Lecture Notes in Artificial Intelligence , vol. 3452 . Springer , 301--331. Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2004. The dependency pair framework: Combining techniques for automated termination proofs. In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence, vol. 3452. Springer, 301--331."},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence","volume":"2850","author":"Giesl J.","unstructured":"Giesl , J. , Thiemann , R. , Schneider-Kamp , P. , and Falke , S . 2003. Improving dependency pairs . In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence , vol. 2850 . Springer, 165 --179. Giesl, J., Thiemann, R., Schneider-Kamp, P., and Falke, S. 2003. Improving dependency pairs. In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artificial Intelligence, vol. 2850. Springer, 165 --179."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273943"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140351"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"Gnaedig I. and Kirchner H. 2007. Narrowing abstraction and constraints for proving properties of reduction relations. In Rewriting Computation and Proof. Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday H. Comon-Lundh et al. Eds. Lecture Notes in Computer Science vol. 4600. Springer 44--67.  Gnaedig I. and Kirchner H. 2007. Narrowing abstraction and constraints for proving properties of reduction relations. In Rewriting Computation and Proof. Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday H. Comon-Lundh et al. Eds. Lecture Notes in Computer Science vol. 4600. Springer 44--67.","DOI":"10.1007\/978-3-540-73147-4_3"},{"key":"e_1_2_2_42_1","unstructured":"Gnaedig I. Kirchner H. and Genet T. 1999. Induction for termination. Tech. rep. 99.R.338 LORIA Nancy France. December.  Gnaedig I. Kirchner H. and Genet T. 1999. Induction for termination. Tech. rep. 99.R.338 LORIA Nancy France. December."},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"Goguen J. Winkler T. Meseguer J. Futatsugi K. and Jouannaud J. 1992. Introducing OBJ3. Tech. rep. Computer Science Laboratory SRI International. March.  Goguen J. Winkler T. Meseguer J. Futatsugi K. and Jouannaud J. 1992. Introducing OBJ3. Tech. rep. Computer Science Laboratory SRI International. March.","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737387"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/2428096.2428097"},{"volume-title":"Proceedings of the 7th Conference on Rewriting Techniques and Applications","author":"Gramlich B.","key":"e_1_2_2_46_1","unstructured":"Gramlich , B. 1996. On proving termination by innermost termination . In Proceedings of the 7th Conference on Rewriting Techniques and Applications , H. Ganzinger, Ed. Lecture Notes in Computer Science, vol. 1103 . Springer , 93--107. Gramlich, B. 1996. On proving termination by innermost termination. In Proceedings of the 7th Conference on Rewriting Techniques and Applications, H. Ganzinger, Ed. Lecture Notes in Computer Science, vol. 1103. Springer, 93--107."},{"key":"e_1_2_2_47_1","volume-title":"-J","author":"Kamin S.","year":"1982","unstructured":"Kamin , S. and L\u00e9vy , J . -J . 1982 . Attempts for generalizing the recursive path ordering. Inria, Rocquencourt . Kamin, S. and L\u00e9vy, J.-J. 1982. Attempts for generalizing the recursive path ordering. Inria, Rocquencourt."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.11.017"},{"key":"e_1_2_2_49_1","unstructured":"Kirchner C. Kirchner H. and Rusinowitch M. 1990. Deduction with symbolic constraints. Revue d'Intelligence Artificielle 4 3 9--52. (Special issue on automatic deduction.)  Kirchner C. Kirchner H. and Rusinowitch M. 1990. Deduction with symbolic constraints. Revue d'Intelligence Artificielle 4 3 9--52. (Special issue on automatic deduction.)"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00215-7"},{"key":"e_1_2_2_51_1","first-page":"210","article-title":"Well-Quasi ordering, the tree theorem and Vazsonyi's conjecture","volume":"95","author":"Kruskal J. B.","year":"1960","unstructured":"Kruskal , J. B. 1960 . Well-Quasi ordering, the tree theorem and Vazsonyi's conjecture . Trans. Amer. Math. Soc. 95 , 210 -- 225 . Kruskal, J. B. 1960. Well-Quasi ordering, the tree theorem and Vazsonyi's conjecture. Trans. Amer. Math. Soc. 95, 210--225.","journal-title":"Trans. Amer. Math. Soc."},{"volume-title":"On proving term rewriting systems are noetherian. Tech. rep","author":"Lankford D. S.","key":"e_1_2_2_52_1","unstructured":"Lankford , D. S. 1979. On proving term rewriting systems are noetherian. Tech. rep ., Louisiana Technical University , Mathematics Deptartment , Ruston Louisiana. Lankford, D. S. 1979. On proving term rewriting systems are noetherian. Tech. rep., Louisiana Technical University, Mathematics Deptartment, Ruston Louisiana."},{"key":"e_1_2_2_53_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 23rd International Colloquium on Automata, Languages and Programming","author":"Lucas S.","unstructured":"Lucas , S. 1996. Termination of context-sensitive rewriting by rewriting . In Proceedings of the 23rd International Colloquium on Automata, Languages and Programming . Lecture Notes in Computer Science , vol. 1099 . Springer , 122--133. Lucas, S. 1996. Termination of context-sensitive rewriting by rewriting. In Proceedings of the 23rd International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 1099. Springer, 122--133."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773194"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/645710.664488"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93176-7"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01190830"},{"key":"e_1_2_2_58_1","volume-title":"Proceedings of the 12th Conference on Compiler Construction, G. Hedin, Ed. Lecture Notes in Computer Science","volume":"2622","author":"Moreau P.-E.","unstructured":"Moreau , P.-E. , Ringeissen , C. , and Vittek , M . 2003. A pattern matching compiler for multiple target languages . In Proceedings of the 12th Conference on Compiler Construction, G. Hedin, Ed. Lecture Notes in Computer Science , vol. 2622 . Springer, 61--76. Moreau, P.-E., Ringeissen, C., and Vittek, M. 2003. A pattern matching compiler for multiple target languages. In Proceedings of the 12th Conference on Compiler Construction, G. Hedin, Ed. Lecture Notes in Computer Science, vol. 2622. Springer, 61--76."},{"volume-title":"Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00)","author":"Nakamura M.","key":"e_1_2_2_59_1","unstructured":"Nakamura , M. and Ogata , K . 2000. The evaluation strategy for head normal form with and without on-demand flags . In Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00) , K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, 211--227. Nakamura, M. and Ogata, K. 2000. The evaluation strategy for head normal form with and without on-demand flags. In Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications (WRLA'00), K. Futatsugi, Ed. Electronic Notes in Theoretical Computer Science, 211--227."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00269-5"},{"key":"e_1_2_2_61_1","series-title":"Lecture Notes in Computer Science","volume-title":"TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Proceedings of the Static Analysis Symposium'97","author":"Panitz S. E.","year":"1997","unstructured":"Panitz , S. E. and Schmidt-Schauss , M. 1997 . TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Proceedings of the Static Analysis Symposium'97 . Lecture Notes in Computer Science , vol. 1302 . Springer , 345--360. Panitz, S. E. and Schmidt-Schauss, M. 1997. TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In Proceedings of the Static Analysis Symposium'97. Lecture Notes in Computer Science, vol. 1302. Springer, 345--360."},{"key":"e_1_2_2_62_1","unstructured":"Plaisted D. 1978. Well-Founded orderings for proving termination of systems of rewrite rules. Tech. rep. R-78-932 Department of Computer Science Univesity of Illinois at Urbana Champaign. July.  Plaisted D. 1978. Well-Founded orderings for proving termination of systems of rewrite rules. Tech. rep. R-78-932 Department of Computer Science Univesity of Illinois at Urbana Champaign. July."},{"volume-title":"Term Rewriting Systems","author":"van Oostrom V.","key":"e_1_2_2_63_1","unstructured":"van Oostrom , V. and de Vrijer , R. 2003. Term Rewriting Systems . Cambridge Tracts in Theoretical Computer Science, vol. 55 . Cambridge University Press , Chapter 9. Strategies. van Oostrom, V. and de Vrijer, R. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Chapter 9. Strategies."},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/647200.718711"},{"key":"e_1_2_2_65_1","series-title":"Lecture Notes in Computer Science","volume-title":"Domain-Specific Program Generation, C. Lengauer et al., Eds","author":"Visser E.","unstructured":"Visser , E. 2004. Program transformation with Stratego\/XT: Rules, strategies, tools, and systems in StrategoXT-0.9 . In Domain-Specific Program Generation, C. Lengauer et al., Eds . Lecture Notes in Computer Science , vol. 3016 . Spinger , 216--238. Visser, E. 2004. Program transformation with Stratego\/XT: Rules, strategies, tools, and systems in StrategoXT-0.9. In Domain-Specific Program Generation, C. Lengauer et al., Eds. Lecture Notes in Computer Science, vol. 3016. Spinger, 216--238."},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/2428096.2428100"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462182","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1462179.1462182","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:15Z","timestamp":1750253415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462182"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":65,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["10.1145\/1462179.1462182"],"URL":"https:\/\/doi.org\/10.1145\/1462179.1462182","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,2]]},"assertion":[{"value":"2006-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}