{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T19:41:04Z","timestamp":1768592464649,"version":"3.49.0"},"reference-count":48,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,4,1]],"date-time":"2000-04-01T00:00:00Z","timestamp":954547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4855,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,4]]},"DOI":"10.1016\/s0304-3975(99)00207-8","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T01:59:23Z","timestamp":1027648763000},"page":"133-178","source":"Crossref","is-referenced-by-count":325,"title":["Termination of term rewriting using dependency pairs"],"prefix":"10.1016","volume":"236","author":[{"given":"Thomas","family":"Arts","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(99)00207-8_BIB1","unstructured":"T. Arts, Termination by absence of infinite chains of dependency pairs, in: H. Kirchner (Ed.), Proc. 21st Internat. Colloquium on Trees in Algebra and Programming, CAAP \u201996, Lecture Notes in Computer Science, vol. 1059, Link\u00f6ping, Sweden, April, Springer, Berlin, 1986, pp. 196\u2013210."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB2","doi-asserted-by":"crossref","unstructured":"T. Arts, Automatically proving termination and innermost normalisation of term rewriting systems, Ph.D. Thesis, Utrecht University, The Netherlands, May 1997.","DOI":"10.1007\/3-540-62950-5_68"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB3","doi-asserted-by":"crossref","unstructured":"T. Arts, J. Giesl, Termination of constructor systems, in: H. Ganzinger (Ed.), Proc. 7th Internat. Conf. on Rewriting Techniques and Applications, RTA-96, Lecture Notes in Computer Science, vol. 1103, New Brunswick, NJ, USA, July, Springer, Berlin, 1996, pp. 63\u201377.","DOI":"10.1007\/3-540-61464-8_43"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB4","doi-asserted-by":"crossref","unstructured":"T. Arts, J. Giesl, Automatically proving termination where simplification orderings fail, in: M. Dauchet (Ed.), Proc. 7th Internat. Joint Conf. on the Theory and Practice of Software Development, TAPSOFT \u201997, Lecture Notes in Computer Science, vol. 1214, Lille, France, April, Springer, Berlin, 1997, pp. 261\u2013272.","DOI":"10.1007\/BFb0030602"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB5","doi-asserted-by":"crossref","unstructured":"T. Arts, J. Giesl, Proving innermost normalisation automatically, in: H. Comon (Ed.), Proc. 8th Internat. Conf. on Rewriting Techniques and Applications, RTA-97, Lecture Notes in Computer Science, vol. 1232, Sitges, Spain, June, Springer, Berlin, 1997, pp. 157\u2013171.","DOI":"10.1007\/3-540-62950-5_68"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB6","unstructured":"T. Arts, J. Giesl, Termination of term rewriting using dependency pairs, Tech. Report IBN 97\/46, Darmstadt University of Technology, Germany, September, 1997. http:\/\/www.inferenzsysteme. informatik.tu-darmstadt.de."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB7","unstructured":"T. Arts, J. Giesl, Modularity of termination using dependency pairs, in: T. Nipkow (Ed.), Proc. 9th Internat. Conf. Rewriting Techniques and Applications, RTA-98, Lecture Notes in Computer Science, vol. 1379, Tsukuba, Japan, March\/April, Springer, Berlin, 1988, pp. 226\u2013240."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB8","unstructured":"T. Arts, H. Zantema, Termination of logic programs using semantic unification, in: M. Proietti (Ed.), Proc. 5th Internat. Workshop on Logic Program Synthesis and Transformation, LoPSTr \u201995, Lecture Notes in Computer Science, vol. 1048, Utrecht, The Netherlands, September, Springer, Berlin, 1995, pp. 219\u2013233."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB9","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz, Commutation, transformation and termination, in: J.H. Siekmann (Ed.), Proc. 8th Internat. Conf. on Automated Deduction, CADE-8, Lecture Notes in Computer Science, vol. 230, Oxford, England, July, Springer, Berlin, 1986, pp. 5\u201320.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB10","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01810293","article-title":"Termination by completion","volume":"1","author":"Bellegarde","year":"1990","journal-title":"Appl. Algebra Eng. Comm. Comput."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB11","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":"Sci. Comput. Programm."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB12","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1007\/BF01209624","article-title":"Proving termination of (conditional) rewrite systems","volume":"30","author":"Bevers","year":"1993","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB13","first-page":"459","article-title":"Recursive applicative program schemes","volume":"vol. B","author":"Courcelle","year":"1990"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB14","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, Termination of linear rewriting systems, in: S. Even, O. Kariv (Eds.), Proc. 8th Internat. Coll. on Automata, Languages and Programming, ICALP \u201981, Lecture Notes in Computer Science, vol. 115, Acre, Israel, July, Springer, Berlin, 1981, pp. 448\u2013458.","DOI":"10.1007\/3-540-10843-2_36"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB15","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":"Theoret. Comput. Sci."},{"issue":"1 and 2","key":"10.1016\/S0304-3975(99)00207-8_BIB16","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"10.1016\/S0304-3975(99)00207-8_BIB17","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","article-title":"Natural termination","volume":"142","author":"Dershowitz","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB18","first-page":"243","article-title":"Rewrite systems","volume":"vol. B","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB19","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF01237233","article-title":"Automating the Knuth Bendix ordering","volume":"28","author":"Dick","year":"1990","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB20","doi-asserted-by":"crossref","unstructured":"M. Ferreira, H. Zantema, Syntactical analysis of total termination, in: G. Levi, M. Rodr\u0131\u0301guez-Artalejo (Eds.), Proc. 4th Internat. Conf. on Algebraic and Logic Programming, ALP \u201994, Lecture Notes in Computer Science, vol. 850, Madrid, Spain, September, Springer, Berlin, 1994, pp. 204\u2013222.","DOI":"10.1007\/3-540-58431-5_15"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB21","doi-asserted-by":"crossref","unstructured":"M. Ferreira, H. Zantema, Dummy Elimination: making termination easier, in: H. Reichel (Ed.), Proc. 10th Internat. Conf. on Fundamentals of Computation Theory, FCT \u201995, Lecture Notes in Computer Science, Dresden, Germany, August, Springer, Berlin, 1995, pp. 243\u2013252.","DOI":"10.1007\/3-540-60249-6_56"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB22","unstructured":"O. Geupel, Overlap closures and termination of term rewriting systems, Tech. Report MIP-8922 283, Universit\u00e4t Passau, Passau, Germany, 1989."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB23","doi-asserted-by":"crossref","unstructured":"J. Giesl, Generating polynomial orderings for termination proofs, in: J. Hsiang (Ed.), Proc. 6th Internat. Conf. on Rewriting Techniques and Applications, RTA-95, Lecture Notes in Computer Science, vol. 914, Kaiserslautern, Germany, April, Springer, Berlin, 1995, pp. 426\u2013431.","DOI":"10.1007\/3-540-59200-8_77"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB24","doi-asserted-by":"crossref","unstructured":"J. Giesl, Termination analysis for functional programs using term orderings, in: A. Mycroft (Ed.), Proc. 2nd Internat. Static Analysis Symp., SAS \u201995, Lecture Notes in Computer Science, vol. 983, Glasgow, UK, September, Springer, Berlin, 1995, pp. 154\u2013171.","DOI":"10.1007\/3-540-60360-3_38"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1005797629953","article-title":"Termination of nested and mutually recursive algorithms","volume":"19","author":"Giesl","year":"1997","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB26","unstructured":"J. Giesl, E. Ohlebusch, Pushing the frontiers of combining rewrite systems farther outwards, in: Proc. 2nd Internat. Workshop on Frontiers of Combining Systems, FroCoS \u201998, Logic and Communication Series Amsterdam, The Netherlands, October, Research Studies Press, John Wiley & Sons, 1999."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB27","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","article-title":"Abstract relations between restricted termination and confluence properties of rewrite systems","volume":"24","author":"Gramlich","year":"1995","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB28","doi-asserted-by":"crossref","unstructured":"B. Gramlich, On proving termination by innermost termination, in: H. Ganzinger (Ed.), Proc. 7th Internat. Conf. on Rewriting Techniques and Applications, RTA-96, Lecture Notes in Computer Science, vol. 1103, New Brunswick, NJ, USA, July, Springer, Berlin, 1996, pp. 93\u2013107.","DOI":"10.1007\/3-540-61464-8_45"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB29","unstructured":"G. Huet, D. Lankford, On the uniform halting problem for term rewriting systems, Tech. Report 283, INRIA, Le Chesnay, France, 1978."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB30","doi-asserted-by":"crossref","unstructured":"J.M. Hullot, Canonical forms and unification, in: W. Bibel, R. Kowalski (Eds.), Proc. 5th Internat. Conf. on Automated Deduction, CADE-5, Lecture Notes in Computer Science, vol. 87, Les Arcs, France, July, Springer, Berlin, 1980, pp. 318\u2013334.","DOI":"10.21236\/ADA087640"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB31","unstructured":"S. Kamin, J.-J. L\u00e9vy, Two generalizations of the recursive path ordering, Department of Computer Science, University of Illinois, IL, 1980."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB32","first-page":"1","article-title":"Term rewriting systems","volume":"vol. 2","author":"Klop","year":"1992"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB33","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB34","unstructured":"T. Kolbe, Challenge problems for automated termination proofs of term rewriting systems, Tech. Report IBN 96\/42, Darmstadt University of Technology, Germany, 1996."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB35","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1016\/0304-3975(95)00075-8","article-title":"Modular proofs for completeness of hierarchical term rewriting systems","volume":"151","author":"Krishna Rao","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB36","unstructured":"M.R.K. Krishna Rao, Some characteristics of strong innermost normalization, in: M. Wirsing, M. Nivat (Eds.), Proc. 5th Internat. Conf. on Algebraic Methodology and Software Technology, AMAST \u201996, Lecture Notes in Computer Science, vol. 1101, Munich, Germany, July, Springer, Berlin, 1996, pp. 406\u2013420."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB37","unstructured":"D.S. Lankford, On proving term rewriting systems are Noetherian, Tech. Report Memo MTP-3, Louisiana Technical University, Ruston, LA, 1979."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB38","unstructured":"D.S. Lankford, D.R. Musser, A finite termination criterion, 1978."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB39","doi-asserted-by":"crossref","unstructured":"C. March\u00e9, X. Urbain, Termination of associative-commutative rewriting by dependency pairs, in: T. Nipkow (Ed.), Proc. 9th Internat. Conf. on Rewriting Techniques and Applications, RTA-98, Lecture Notes in Computer Science, vol. 1397, Tsukuba, Japan, March\/April, Springer, Berlin, 1998, pp. 241\u2013255.","DOI":"10.1007\/BFb0052374"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB40","doi-asserted-by":"crossref","unstructured":"A. Middeldorp, H. Ohsaki, H. Zantema, Transforming termination by self-labelling, in: M.A. McRobbie, J.K. Slaney (Eds.), Proc. 13th Internat. Conf. on Automated Deduction, CADE-13, Lecture Notes in Artificial Intelligence, vol. 1104, New Brunswick, NJ, USA, July\/August, Springer, Berlin, 1996, pp. 373\u2013387.","DOI":"10.1007\/3-540-61511-3_101"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB41","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0304-3975(96)00172-7","article-title":"Simple termination of rewrite systems","volume":"175","author":"Middeldorp","year":"1997","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB42","unstructured":"D.A. Plaisted, A recursively defined ordering for proving termination of term rewriting systems, Tech. Report R-78-943, Department of Computer Science, University of Illinois, Urbana-Champaign, IL, 1978."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB43","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","article-title":"Generating polynomial orderings","volume":"49","author":"Steinbach","year":"1994","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB44","doi-asserted-by":"crossref","unstructured":"J. Steinbach, Automatic termination proofs with transformation orderings, in: J. Hsiang (Ed.), Proc. 6th Internat. Conf. on Rewriting Techniques and Applications, RTA-95, Lectures Notes in Computer Science, vol. 914, Kaiserslautern, Germany, April, Springer, Berlin, 1995, pp. 11\u201325. Full Version appeared as Tech. Report SR-92-23, Universit\u00e4t Kaiserslautern, Germany, 1992.","DOI":"10.1007\/3-540-59200-8_44"},{"key":"10.1016\/S0304-3975(99)00207-8_BIB45","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/FI-1995-24123","article-title":"Simplification orderings: history of results","volume":"24","author":"Steinbach","year":"1995","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB46","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","article-title":"Counterexamples to the termination for the direct sum of term rewriting systems","volume":"25","author":"Toyama","year":"1987","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB47","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","article-title":"Termination of term rewriting: interpretation and type elimination","volume":"17","author":"Zantema","year":"1994","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(99)00207-8_BIB48","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":"Fund. Inform."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599002078?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599002078?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T00:47:15Z","timestamp":1580863635000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599002078"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,4]]},"references-count":48,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,4]]}},"alternative-id":["S0304397599002078"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00207-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,4]]}}}