{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:55Z","timestamp":1761610375528,"version":"build-2065373602"},"reference-count":61,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4958,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2000]]},"DOI":"10.1016\/s1571-0661(05)80124-0","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"93-120","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Termination and normalisation under strategy Proofs in ELAN"],"prefix":"10.1016","volume":"36","author":[{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"first","affiliation":[]},{"given":"Isabelle","family":"Gnaedig","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80124-0_BIBAG97A","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In M. Bidoit and M. Dauchet, editors, TAPSOFT'97: Theory and Practice of Software Development, Proceedings of 7th International Joint Conference CAAP\/FASE, volume 1214 of Lecture Notes in Computer Science, pages 261\u2013272. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030602"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBAG97B","doi-asserted-by":"crossref","unstructured":"T. Arts and J. Giesl. Proving innermost termination automatically. In Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), volume 1232 of Lecture Notes in Computer Science, pages 157\u2013171. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-62950-5_68"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBAG00","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","article-title":"Termination of term rewriting using dependency pairs","volume":"236","author":"Arts","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBAN00","unstructured":"C. Alvarado and Quang-Huy Nguyen. Elan for equational reasoning in Coq. In J. Despeyroux, editor, Proceedings of the Workshop on Logical Frameworks and Meta-languages, Santa Barbara (California), June 2000."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBART97","unstructured":"T. Arts. Automatically proving termination and innermost normalisation of term rewriting systems. PhD thesis, Utrecht University, The Netherlands, 1997."},{"issue":"2","key":"10.1016\/S1571-0661(05)80124-0_BIBBCL87","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","article-title":"Termination of rewriting systems by polynomial interpretations and its implementation","volume":"9","author":"Ben Cherifa","year":"1987","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(05)80124-0_BKK96","doi-asserted-by":"crossref","unstructured":"P. Borovansk\u00fd, C. Kirchner, H. Kirchner, P-E. Moreau, and M. Vittek. ELAN: A logical framework based on computational systems. In Jos\u00e9 Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4 of Electronic Notes in TCS, Asilomar (California), September 1996.","DOI":"10.1016\/S1571-0661(04)00032-5"},{"key":"10.1016\/S1571-0661(05)80124-0_BKK98","doi-asserted-by":"crossref","unstructured":"P. Borovansky, C. Kirchner, H. Kirchner, P-E. Moreau, and C. Ringeissen. An overview of ELAN. In C. and H. Kirchner, editors, Proceedings of the second International Workshop on Rewriting Logic and Applications, Pont-\u00e0-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science, volume 15. http:\/\/www.elsevier.nl\/locate\/entcs\/volumel5.html.","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBBKKR01","doi-asserted-by":"crossref","DOI":"10.1142\/S0129054101000412","article-title":"Rewriting with strategies in ELAN: a functional semantics","author":"Borovansk\u00fd, C. Kirchner","year":"2001","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(05)80124-0_BIBBL90","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01810293","article-title":"Termination by completion","volume":"1","author":"Bellegarde","year":"1990","journal-title":"Applicable Algebra in Engineering, Communication and Computation"},{"year":"1998","series-title":"Term Rewriting and all That","author":"Baader","key":"10.1016\/S1571-0661(05)80124-0_BIBBN98"},{"year":"1997","series-title":"Tree automata techniques and applications","author":"Comon","key":"10.1016\/S1571-0661(05)80124-0_CDG97"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBCDGV91","doi-asserted-by":"crossref","unstructured":"J.L. Coquid\u00e9, M. Dauchet, R. Gilleron, and S. V\u00b4gv\u00f6lgyi. Bottom-up tree pushdown automata and rewrite systems. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 287\u2013298. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53904-2_104"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBCELM96","unstructured":"M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, (Asilomar, Pacific Grove, CA, USA), volume 5 of Electronic Notes in Theoretical Computer Science. North Holland, September 1996."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBCK99","first-page":"95","article-title":"Combining higher-order and first-order computation using \u03c1-calculus: Towards a semantics of ELAN","volume":"0863802524","author":"Cirstea","year":"1999"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBCM96","unstructured":"M. Clavel and J. Meseguer. Reflection and Strategies in Rewriting Logic. In J. Meseguer, editor, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, (Asilomar, Pacific Grove, CA, USA), volume 5 of Electronic Notes in Theoretical Computer Science. North Holland, September 1996."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBCR87","article-title":"How to characterize the language of ground normal forms","author":"Comon","year":"1987","journal-title":"Technical Report 676, INRIA-Lorraine"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBDER82","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBDER94","doi-asserted-by":"crossref","unstructured":"N. Dershowitz. Hierarchical termination. In Proceedings 4-th International Workshop on Conditional Term Rewriting Systems, Jerusalem (Israel), volume 968 of Lecture Notes in Computer Science, pages 89\u2013105. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-60381-6_6"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBDH95","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","article-title":"Natural termination","volume":"142(2)","author":"Dershowitz","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBDJ90","first-page":"244","article-title":"Handbook of Theoretical Computer Science","author":"Dershowitz","year":"1990","journal-title":"volume B, chapter 6: Rewrite Systems. Elsevier Science Publishers B. V. (North-Holland). Also as: Research report 478, LRI"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBDT90","doi-asserted-by":"crossref","unstructured":"M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proceedings 5th IEEE Symposium on Logic in Computer Science, Philadelphia (Pa., USA), pages 242\u2013248, June 1990.","DOI":"10.1109\/LICS.1990.113750"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBFN97","unstructured":"K. Futatsugi and A. Nakagawa. An overview of CAFE specification environment - an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In Proceedings of the 1st IEEE Int. Conference on Formal Engineering Methods, 1997."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGB85","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(85)90089-1","article-title":"Reductions in tree replacement systems","volume":"37","author":"Gallier","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGEN97","article-title":"Proving termination of sequential reduction relation using tree automata","author":"Genet","year":"1997","journal-title":"Technical Report 97-R-091, Centre de Recherche en Informatique de Nancy"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGEN98","doi-asserted-by":"crossref","unstructured":"T. Genet. Decidable approximations of sets of descendants and sets of normal forms. In Proceedings 9th Conference on Rewriting Techniques and Applications, Tsukuba (Japan), volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0052368"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGG97","doi-asserted-by":"crossref","unstructured":"T. Genet and I. Gnaedig. Termination proofs using gpo ordering constraints. In M. Dauchet, editor, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, Lille (France), volume 1214 of Lecture Notes in Computer Science, pages 249-260. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030601"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGK00","doi-asserted-by":"crossref","unstructured":"T. Genet and F. Klay. Rewriting for cryptographic protocol verification. In Proceedings International Conference on Automated Deduction, CADE-17. Springer-Verlag, LNAI, 2000.","DOI":"10.1007\/10721959_21"},{"year":"2000","series-title":"Induction for termination","author":"Gnaedig","key":"10.1016\/S1571-0661(05)80124-0_BIBGKF00"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGMW79","series-title":"volume 78 of Lecture Notes in Computer Science.","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","article-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"Gordon","year":"1979"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGRA94","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/BF01190827","article-title":"Generalized sufficient conditions for modular termination of rewriting","volume":"5","author":"Gramlich","year":"1994","journal-title":"Applicable Algebra in Engineering, Communication and Computation"},{"issue":"1","key":"10.1016\/S1571-0661(05)80124-0_BIBGRA96","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(96)00042-4","article-title":"On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems","volume":"165","author":"Gramlich","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGRA97","series-title":"Proc. 12th Int. Workshop on Algebraic Development Techniques, WADT'97 (Abstracts)","article-title":"Modular aspects of rewrite-based specifications","author":"Gramlich","year":"1997"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGS84","unstructured":"F. G\u00e9cseg and M. Steinby. Tree automata. Akademiai Kiado, Budapest, Hungary, 1984."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBGT95","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/FI-1995-24127","article-title":"Regular tree languages and rewrite systems","volume":"24","author":"Gilleron","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBHCS96","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/S0743-1066(96)00068-4","article-title":"The execution algorithm of Mercury, an efficient purely declarative logic programming language","volume":"29","author":"Henderson","year":"1996","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBHSC96","unstructured":"F. Henderson, Z. Somogyi, and T. Conway. Determinism analysis in the Mercury compiler. In Proceedings of the Nineteenth Australian Computer Science Conference, pages 337-346, Melbourne, Australia, January 1996."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBJAC96","doi-asserted-by":"crossref","unstructured":"F. Jacquemard. Decidable approximations of term rewriting systems. In H. Ganzinger, editor, Proceedings 7th Conference on Rewriting Techniques and Applications, New Brunswick (New Jersey, USA), pages 362-376. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61464-8_65"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKIR99","first-page":"273","article-title":"Term Rewriting","author":"Kirchner","year":"1999","journal-title":"chapter 9. IFIP State-of-the-Art Reports. Springer. Report LORIA 99-R-098"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKK90","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(90)90221-I","article-title":"Modular term rewriting systems and the termination","volume":"34","author":"Kurihara","year":"1990","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKK99","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Rewriting, solving, proving. A preliminary version of a book available at http:\/\/www.loria.fr\/~ckirchne\/rsp.ps.gz, 1999.","DOI":"10.1007\/978-3-642-59851-7_9"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKL80","article-title":"Attempts for generalizing the recursive path ordering","author":"Kamin","year":"1980","journal-title":"Unpublished manuscript"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBK1193","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1145\/151257.151260","article-title":"A meta-environment for generating programming environments","volume":"2","author":"Klint","year":"1993","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKM98","doi-asserted-by":"crossref","unstructured":"H. Kirchner and P-E Moreau. Non-deterministic computations in ELAN. In J.L. Fiadeiro, editor, Recent Developements in Algebraic Specification Techniques, Proc. 13th WADT'98, Selected Papers, number 1548 in Lecture Notes in Computer Science, pages 168-182. Springer-Verlag, 1998. Report LORIA 98-R-278.","DOI":"10.1007\/3-540-48483-3_12"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBKM00","article-title":"Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories","author":"Kirchner","year":"2000","journal-title":"Journal of Functional Programming"},{"issue":"3","key":"10.1016\/S1571-0661(05)80124-0_BIBKO91","first-page":"357","article-title":"Modular term rewriting systems with shared constructors","volume":"14","author":"Kurihara","year":"1991","journal-title":"Journal of Information Processing of Japan"},{"issue":"2","key":"10.1016\/S1571-0661(05)80124-0_BIBKR95","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/0304-3975(95)00075-8","article-title":"Modular proofs for completeness of herarchical term rewriting systems","volume":"151","author":"Krishna Rao","year":"1995","journal-title":"Theoretical Computer Science"},{"year":"1979","series-title":"On proving term rewriting systems are noetherian. Technical report, Louisiana Tech.","author":"Lankford","key":"10.1016\/S1571-0661(05)80124-0_BIBLAN79"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBMID90","unstructured":"A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, 1990."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBMT91","doi-asserted-by":"crossref","unstructured":"A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), 1991. also Report CS-R9058, CWI, 1990.","DOI":"10.1007\/3-540-53904-2_96"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBOCM00","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch, C. Claves, and C. Marche. TALP: a tool for the termination analysis of logic programs. In Proceedings 11th Conference on Rewriting Techniques and Applications, Norwich (UK), volume 1833 of Lecture Notes in Computer Science, pages 270-273. Springer-Verlag, 2000.","DOI":"10.1007\/10721975_20"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBOHL94","unstructured":"E. Ohlebusch. Modular Properties of Composable Term Rewriting Systems. PhD thesis, Universit\u00e4t Bielefeld, Bielefeld, 1994."},{"key":"10.1016\/S1571-0661(05)80124-0_BIBPAU94","series-title":"volume 828 of Lecture Notes in Computer Science.","article-title":"Isabelle: A Generic Theorem Prover","author":"Paulson","year":"1994"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBPLA78","article-title":"A recursively defined ordering for proving termination of term rewriting systems. Technical Report R-78-943, U.","author":"Plaisted","year":"1978","journal-title":"of Illinois, Dept of Computer Science"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBPLO77","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(05)80124-0_BIBRUS87","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","article-title":"On termination of the direct sum of term rewriting systems","volume":"26","author":"Rusinowitch","year":"1987","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBSAL88","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/0022-0000(88)90014-1","article-title":"Deterministic Tree Pushdown Automata and Monadic Tree Rewriting Systems","volume":"37","author":"Salomaa","year":"1988","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBST85","unstructured":"H. Sawamura and T. Takeshima. Recursive unsolvability of determinacy, solvable cases of determinacy and their applications to Prolog optimization. In Proceedings of the Second International Logic Programming Conference, pages 200-207, Boston, Massachusetts, 1985."},{"issue":"1","key":"10.1016\/S1571-0661(05)80124-0_BIBTOY87","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","article-title":"On the church-rosser property for the direct sum of term rewritig systens","volume":"34","author":"Toyama","year":"1987","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBVB98","doi-asserted-by":"crossref","unstructured":"E. Visser and Z. Benaissa. A core language for rewriting. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, editors, Proceedings of the second International Workshop on Rewriting Logic and Applications, volume 15, Pont-\u00e0-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science, http:\/\/www.elsevier.nl\/locate\/entcs\/volumel5.html","DOI":"10.1016\/S1571-0661(05)80027-1"},{"key":"10.1016\/S1571-0661(05)80124-0_BIBZAN95","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","article-title":"Termination of term rewriting by semantic labelling","volume":"24","author":"Zantema","year":"1995","journal-title":"Fundamenta Informaticae"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801240?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801240?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:23Z","timestamp":1761610103000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105801240"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":61,"alternative-id":["S1571066105801240"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80124-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Termination and normalisation under strategy Proofs in ELAN","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80124-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}