{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T19:52:03Z","timestamp":1768593123491,"version":"3.49.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,1,10]],"date-time":"2007-01-10T00:00:00Z","timestamp":1168387200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,23]]},"DOI":"10.1007\/s10817-006-9057-7","type":"journal-article","created":{"date-parts":[[2007,1,9]],"date-time":"2007-01-09T14:17:15Z","timestamp":1168352235000},"page":"155-203","source":"Crossref","is-referenced-by-count":133,"title":["Mechanizing and Improving Dependency Pairs"],"prefix":"10.1007","volume":"37","author":[{"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Falke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,1,10]]},"reference":[{"key":"9057_CR1","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133\u2013178 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9057_CR2","unstructured":"Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Technical report AIB-2001-09, RWTH Aachen, Germany. Available from http:\/\/aib.informatik.rwth-aachen.de (2001)"},{"key":"9057_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge, UK (1998)"},{"key":"9057_CR4","unstructured":"Borralleras, C.: Ordering-based methods for proving termination automatically. Ph.D. thesis, Universitat Polit\u00e8cnica de Catalunya, Spain (2003)"},{"key":"9057_CR5","doi-asserted-by":"crossref","unstructured":"Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: Proceedings of the 17th CADE. LNAI 1831, pp. 346\u2013364 (2000)","DOI":"10.1007\/10721959_27"},{"key":"9057_CR6","unstructured":"Contejean, E., March\u00e9, C., Monate, B., Urbain, X.: CiME version 2. Available from http:\/\/cime.lri.fr (2000)"},{"key":"9057_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3, 69\u2013116 (1987)","journal-title":"J. Symb. Comput."},{"issue":"1\u20132","key":"9057_CR8","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/s002000100065","volume":"12","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput. 12(1\u20132), 117\u2013156 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"3\u20134","key":"9057_CR9","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/s00200-004-0162-8","volume":"15","author":"A. Geser","year":"2004","unstructured":"Geser, A., Hofbauer, D., Waldmann, J.: Match-bounded string rewriting systems. Appl. Algebra Eng. Commun. Comput. 15(3\u20134), 149\u2013171 (2004)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9057_CR10","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Generating polynomial orderings for termination proofs. In: Proceedings of the 6th RTA. LNCS 914, pp. 426\u2013431 (1995)","DOI":"10.1007\/3-540-59200-8_77"},{"issue":"1\u20132","key":"9057_CR11","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s002000100063","volume":"12","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12(1\u20132), 39\u201372 (2001)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"1","key":"9057_CR12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. J. Symb. Comput. 34(1), 21\u201358 (2002)","journal-title":"J. Symb. Comput."},{"key":"9057_CR13","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Proceedings of the 10th LPAR, LNAI 2850. pp. 165\u2013179 (2003a)","DOI":"10.1007\/978-3-540-39813-4_11"},{"key":"9057_CR14","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing dependency pairs. Technical report AIB-2003-08, RWTH Aachen, Germany. Available from http:\/\/aib.informatik.rwth-aachen.de (2003b)"},{"key":"9057_CR15","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of the 11th LPAR. LNAI 3452, pp. 301\u2013331 (2005a)","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"9057_CR16","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proceedings of the 5th FroCoS. LNAI 3717, pp. 216\u2013231 (2005b)","DOI":"10.1007\/11559306_12"},{"key":"9057_CR17","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Proceedings of the 3rd IJCAR. LNAI 4130, pp. 281\u2013286 (2006a)","DOI":"10.1007\/11814771_24"},{"key":"9057_CR18","doi-asserted-by":"crossref","unstructured":"Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for Haskell: from term rewriting to programming languages. In: Proceedings of the 17th RTA. LNCS 4098, pp. 297\u2013312 (2006b)","DOI":"10.1007\/11805618_23"},{"key":"9057_CR19","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/BF01190827","volume":"5","author":"B. Gramlich","year":"1994","unstructured":"Gramlich, B.: Generalized sufficient conditions for modular termination of rewriting. Appl. Algebra Eng. Commun. Comput. 5, 131\u2013158 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9057_CR20","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","volume":"24","author":"B. Gramlich","year":"1995","unstructured":"Gramlich, B.: Abstract relations between restricted termination and confluence properties of rewrite systems. Fundam. Inform. 24, 3\u201323 (1995)","journal-title":"Fundam. Inform."},{"key":"9057_CR21","unstructured":"Gramlich, B.: Termination and confluence properties of structured rewrite systems. Ph.D. thesis, Universit\u00e4t Kaiserslautern, Germany (1996)"},{"key":"9057_CR22","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proceedings of the 15th RTA. LNCS 3091, pp. 249\u2013268 (2004a)","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"9057_CR23","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Proceedings of the AISC\u00a0\u201904, LNAI 3249, 185\u2013198 (2004b)","DOI":"10.1007\/978-3-540-30210-0_16"},{"key":"9057_CR24","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool. In: Proceedings of the 16th RTA. LNCS 3467, pp. 175\u2013184 (2005a)","DOI":"10.1007\/978-3-540-32033-3_14"},{"issue":"1\u20132","key":"9057_CR25","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Inf. Comput. 199(1\u20132), 172\u2013199 (2005b)","journal-title":"Inf. Comput."},{"issue":"1","key":"9057_CR26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H., Jaku\u0161, D.: Testing positiveness of polynomials. J. Autom. Reason. 21(1), 23\u201338 (1998)","journal-title":"J. Autom. Reason."},{"key":"9057_CR27","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci. 25, 239\u2013299 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"9057_CR28","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford, UK (1970)"},{"key":"9057_CR29","doi-asserted-by":"crossref","unstructured":"Koprowski, A.: TPA: termination proved automatically. In: Proceedings of the 17th RTA. LNCS 4098, pp. 257\u2013266 (2006)","DOI":"10.1007\/11805618_19"},{"key":"9057_CR30","doi-asserted-by":"crossref","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Proceedings of the 1st PPDP. LNCS 1702, pp. 48\u201362 (1999)","DOI":"10.1007\/10704567_3"},{"key":"9057_CR31","unstructured":"Lankford, D.: On proving term rewriting systems are Noetherian. Technical report MTP-3, Louisiana Technical University, Ruston, LA (1979)"},{"key":"9057_CR32","doi-asserted-by":"crossref","unstructured":"Lee, C.\u00a0S., Jones, N. D., Ben-Amram, A.\u00a0M.: The size-change principle for program termination. In: Proceedings of the 28th POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"issue":"3","key":"9057_CR33","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1051\/ita:2005029","volume":"39","author":"S. Lucas","year":"2005","unstructured":"Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theor. Inform. Appl. 39(3), 547\u2013586 (2005)","journal-title":"RAIRO Theor. Inform. Appl."},{"key":"9057_CR34","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Proceedings of the 1st IJCAR. LNAI 2083, pp. 593\u2013610 (2001)","DOI":"10.1007\/3-540-45744-5_49"},{"key":"9057_CR35","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximations for strategies and termination. In: Proceedings of the 2nd WRS. ENTCS 70(6) (2002)","DOI":"10.1016\/S1571-0661(04)80598-X"},{"key":"9057_CR36","doi-asserted-by":"crossref","unstructured":"Ohlebusch, E., Claves, C., March\u00e9, C.: TALP: A tool for termination analysis of logic programs. In: Proceedings of the 11th RTA. LNCS 1833, 270\u2013273 (2000)","DOI":"10.1007\/10721975_20"},{"key":"9057_CR37","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin Heidelberg New York (2002)"},{"key":"9057_CR38","doi-asserted-by":"crossref","unstructured":"Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs by term rewriting. In: Proceedings of the 16th LOPSTR. LNCS (2007) (to appear)","DOI":"10.1007\/978-3-540-71410-1_13"},{"key":"9057_CR39","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of the 2nd IJCAR. LNAI 3097, pp. 75\u201390 (2004)","DOI":"10.1007\/978-3-540-25984-8_4"},{"issue":"4","key":"9057_CR40","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput. 16(4), 229\u2013270 (2005)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9057_CR41","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Inf. Process. Lett. 25, 141\u2013143 (1987)","journal-title":"Inf. Process. Lett."},{"key":"9057_CR42","unstructured":"TPDB web page. http:\/\/www.lri.fr\/~marche\/termination-competition\/"},{"issue":"4","key":"9057_CR43","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF03177743","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain, X.: Modular and incremental automated termination proofs. J. Autom. Reason. 32(4), 315\u2013355 (2004)","journal-title":"J. Autom. Reason."},{"key":"9057_CR44","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"Zantema, H.: Termination of term rewriting by semantic labelling. Fundam. Inform. 24, 89\u2013105 (1995)","journal-title":"Fundam. Inform."},{"issue":"2","key":"9057_CR45","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s10817-005-6545-0","volume":"34","author":"H. Zantema","year":"2005","unstructured":"Zantema, H.: Termination of string rewriting proved automatically. J. Autom. Reason. 34(2), 105\u2013139 (2005)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9057-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9057-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9057-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T17:18:31Z","timestamp":1587316711000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9057-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,1,10]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,1,23]]}},"alternative-id":["9057"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9057-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,1,10]]}}}