{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,1]],"date-time":"2024-09-01T01:50:35Z","timestamp":1725155435777},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,6,22]],"date-time":"2005-06-22T00:00:00Z","timestamp":1119398400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[2005,9]]},"DOI":"10.1007\/s00200-005-0179-7","type":"journal-article","created":{"date-parts":[[2005,6,27]],"date-time":"2005-06-27T14:32:43Z","timestamp":1119882763000},"page":"229-270","source":"Crossref","is-referenced-by-count":27,"title":["The size-change principle and dependency pairs for termination of term rewriting"],"prefix":"10.1007","volume":"16","author":[{"given":"Ren\u00e9","family":"Thiemann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,22]]},"reference":[{"key":"179_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, H., Khoo, S. C.: Affine-based size-change termination. In: Proc. 1st APLAS, LNCS 2895, 2003, pp 122\u2013140","DOI":"10.1007\/978-3-540-40018-9_9"},{"key":"179_CR2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science,"},{"key":"179_CR3","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, 2001. Available from http:\/\/aib.informatik.rwth-aachen.de"},{"key":"179_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, 1998","DOI":"10.1017\/CBO9781139172752"},{"key":"179_CR5","doi-asserted-by":"crossref","unstructured":"Borralleras, C., Ferreira, M., Rubio, A.: Complete monotonic semantic path orderings. In: Proc. 17th CADE, LNAI 1831, 2000, pp 346\u2013364","DOI":"10.1007\/10721959_27"},{"key":"179_CR6","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation, 3, 69\u2013116 (1987)","journal-title":"Journal of Symbolic Computation,"},{"key":"179_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: 33 examples of termination. In: Proc. French Spring School of Theoretical Computer Science, LNCS 909, 1995, pp 16\u201326","DOI":"10.1007\/3-540-59340-3_2"},{"key":"179_CR8","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s002000100065","volume":"12","author":"Dershowitz","year":"2001","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing, 12(1,2), 117\u2013156 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing,"},{"key":"179_CR9","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Cariboo: An induction based proof tool for termination with strategies. In: Proc. 4th PPDP, pp 62\u201373. ACM Press, 2002"},{"key":"179_CR10","first-page":"2","volume":"12","author":"Giesl","year":"2001","unstructured":"Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Applicable Algebra in Engineering, Communication and Computing, 12(1,2), 39\u201372 (2001)","journal-title":"Applicable Algebra in Engineering, Communication and Computing,"},{"key":"179_CR11","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"Giesl","year":"1","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. Journal of Symbolic Computation, 34(1), 21\u201358 (2002)","journal-title":"Journal of Symbolic Computation,"},{"key":"179_CR12","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Proc. 10th LPAR, LNAI 2850, 2003, pp 165\u2013179","DOI":"10.1007\/978-3-540-39813-4_11"},{"key":"179_CR13","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: Proc. 15th RTA, LNCS 3091, 2004, pp 210\u2013220","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"179_CR14","unstructured":"Hirokawa, N., Middeldorp, A.: Approximating dependency graphs without using tree automata techniques. In: Proc. 6th WST, 2003"},{"key":"179_CR15","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. In: Proc. 19th CADE, LNAI 2741, pages 32\u201346, 2003. Full version to appear in Information and Computation","DOI":"10.1007\/978-3-540-45085-6_4"},{"key":"179_CR16","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proc. 15th RTA, LNCS 3091, 2004, pp 249\u2013268","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"179_CR17","unstructured":"Kamin, S., L\u00e9vy, J. J.: Two generalizations of the recursive path ordering. Unpublished Manuscript, University of Illinois, IL, USA, 1980"},{"key":"179_CR18","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, 1970"},{"key":"179_CR19","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00021-X","volume":"183","author":"Korovin","year":"2003","unstructured":"Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. Information and Computation, 183, 165\u2013186 (2003)","journal-title":"Information and Computation,"},{"key":"179_CR20","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M. S., Narendran, P.: On recursive path ordering. Theoretical Computer Science, 40, 323\u2013328 (1985)","journal-title":"Theoretical Computer Science,"},{"key":"179_CR21","doi-asserted-by":"crossref","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Proc. 1st PPDP, LNCS 1702, 1999, pp 48\u201362","DOI":"10.1007\/10704567_3"},{"key":"179_CR22","unstructured":"Lankford, D.: On proving term rewriting systems are Noetherian. Technical Report MTP-3, Louisiana Technical University, Ruston, LA, USA, 1979"},{"key":"179_CR23","doi-asserted-by":"crossref","unstructured":"Lee, C. S.: Program termination analysis in polynomial time. In: Proc. 1st GPCE, LNCS 2487, 2002, pp 218\u2013235","DOI":"10.1007\/3-540-45821-2_14"},{"key":"179_CR24","doi-asserted-by":"crossref","unstructured":"Lee, C. S., Jones, N. D., Ben-Amram, A. M.: The size-change principle for program termination. In: Proc. 28th POPL, 2001, pp 81\u201392","DOI":"10.1145\/360204.360210"},{"key":"179_CR25","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proc. 3rd Hawaii International Conference on System Science, 1970, pp 789\u2013792"},{"key":"179_CR26","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximations for strategies and termination. In: Proc. WRS '02, ENTCS 70(6), 2002","DOI":"10.1016\/S1571-0661(04)80598-X"},{"key":"179_CR27","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"Savitch","year":"2","unstructured":"Savitch, J. W.: Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2), 177\u2013192 (1970)","journal-title":"Journal of Computer and System Sciences,"},{"key":"179_CR28","doi-asserted-by":"crossref","unstructured":"Steinbach, J.: Automatic termination proofs with transformation orderings. In: Proc. 6th RTA, LNCS 914, 1995, pp 11\u201325. Full version appeared as Technical Report SR-92-23, Universit\u00e4t Kaiserslautern, Germany","DOI":"10.1007\/3-540-59200-8_44"},{"key":"179_CR29","unstructured":"Thiemann, R., Giesl, J.: Empirical evaluation of the size-change principle for term rewriting. Available from http:\/\/www.-i2.informatik.rwth-aachen.de\/AProVE\/empiricalSCP.ps"},{"key":"179_CR30","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J.: Size-change termination for term rewriting. In: Proc. 14th RTA, LNCS 2706, 2003, pp 264\u2013278","DOI":"10.1007\/3-540-44881-0_19"},{"key":"179_CR31","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proc. 2nd IJCAR, LNAI 3097, 2004, pp 75\u201390","DOI":"10.1007\/978-3-540-25984-8_4"},{"key":"179_CR32","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters, 25, 141\u2013143 (1987)","journal-title":"Information Processing Letters,"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0179-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00200-005-0179-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0179-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T23:07:02Z","timestamp":1586300822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00200-005-0179-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6,22]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,9]]}},"alternative-id":["179"],"URL":"https:\/\/doi.org\/10.1007\/s00200-005-0179-7","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6,22]]}}}