{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:55Z","timestamp":1775873515646,"version":"3.50.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,2]],"date-time":"2013-03-02T00:00:00Z","timestamp":1362182400000},"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":[[2013,6]]},"DOI":"10.1007\/s10817-013-9277-6","type":"journal-article","created":{"date-parts":[[2013,3,2]],"date-time":"2013-03-02T04:12:33Z","timestamp":1362197553000},"page":"27-56","source":"Crossref","is-referenced-by-count":36,"title":["Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs"],"prefix":"10.1007","volume":"51","author":[{"given":"Lars","family":"Noschinski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabian","family":"Emmes","sequence":"additional","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":[[2013,3,2]]},"reference":[{"key":"9277_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. Comp. Sci. 236, 133\u2013178 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"9277_CR2","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schnabl, A.: Automated implicit computational complexity analysis. In: Proc. IJCAR\u00a0\u201908, LNAI 5195, pp. 132\u2013138 (2008)","DOI":"10.1007\/978-3-540-71070-7_10"},{"key":"9277_CR3","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G.: Dependency pairs and polynomial path orders. In: Proc. RTA\u00a0\u201909, LNCS 5595, pp. 48\u201362 (2009)","DOI":"10.1007\/978-3-642-02348-4_4"},{"key":"9277_CR4","unstructured":"Avanzini, M., Moser, G.: Closing the gap between runtime complexity and polytime computability. In: Proc. RTA \u201910, LIPIcs 6, pp. 33\u201348 (2010)"},{"key":"9277_CR5","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G.: Complexity analysis by graph rewriting. In: Proc. FLOPS \u201910, LNCS 6009, pp. 257\u2013271 (2010)","DOI":"10.1007\/978-3-642-12251-4_19"},{"key":"9277_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: erm Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"issue":"1","key":"9277_CR7","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0956796800003877","volume":"11","author":"G Bonfante","year":"2001","unstructured":"Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Program. 11(1), 33\u201353 (2001)","journal-title":"J. Funct. Program."},{"key":"9277_CR8","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Proc. CAV \u201912, LNCS, pp.\u00a0105\u2013122 (2012)","DOI":"10.1007\/978-3-642-31424-7_13"},{"issue":"2\u20133","key":"9277_CR9","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2\u20133), 195\u2013220 (2008)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9277_CR10","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1016\/j.ic.2006.08.007","volume":"205","author":"A Geser","year":"2007","unstructured":"Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. Inf. Comput. 205(4), 512\u2013534 (2007)","journal-title":"Inf. Comput."},{"key":"9277_CR11","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Proc. LPAR \u201904, LNAI 3452, pp. 301\u2013331 (2005)","DOI":"10.1007\/978-3-540-32275-7_21"},{"issue":"3","key":"9277_CR12","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155\u2013203 (2006)","journal-title":"J. Autom. Reason."},{"key":"9277_CR13","doi-asserted-by":"crossref","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7:1\u20137:39(2011)","DOI":"10.1145\/1890028.1890030"},{"key":"9277_CR14","doi-asserted-by":"crossref","unstructured":"Giesl, J., Str\u00f6der, T., Schneider-Kamp, P., Emmes, F., Fuhs, C.: Symbolic evaluation graphs and term rewriting \u2013 A general methodology for analyzing logic programs. In: Proc. PPDP \u201912, pp. 1\u201312. ACM Press (2012)","DOI":"10.1145\/2370776.2370778"},{"issue":"4","key":"9277_CR15","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1145\/566385.566387","volume":"3","author":"R Givan","year":"2002","unstructured":"Givan, R., McAllester, D.A.: Polynomial-time computation via local inference relations. ACM Trans. Comput. Log. 3(4), 521\u2013541 (2002)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1,2","key":"9277_CR16","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,2), 172\u2013199 (2005)","journal-title":"Inf. Comput."},{"key":"9277_CR17","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proc. IJCAR\u00a0\u201908, LNAI 5195, pp. 364\u2013379 (2008)","DOI":"10.1007\/978-3-540-71070-7_32"},{"key":"9277_CR18","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Moser, G.: Complexity, graphs, and the dependency pair method. In: Proc. LPAR \u201908, LNAI 5330, pp. 652\u2013666 (2008)","DOI":"10.1007\/978-3-540-89439-1_45"},{"key":"9277_CR19","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. CoRR http:\/\/arxiv.org\/abs\/1102.3129 (2011)"},{"key":"9277_CR20","doi-asserted-by":"crossref","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proc. RTA \u201989, LNCS 355, pp. 167\u2013177 (1989)","DOI":"10.1007\/3-540-51081-8_107"},{"key":"9277_CR21","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: Proc. LICS \u201999, pp. 464\u2013473. IEEE Press (1999)","DOI":"10.1109\/LICS.1999.782641"},{"issue":"2","key":"9277_CR22","first-page":"357","volume":"19","author":"A Koprowski","year":"2009","unstructured":"Koprowski, A., Waldmann, J.: Max\/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357\u2013392 (2009)","journal-title":"Acta Cybern."},{"key":"9277_CR23","doi-asserted-by":"crossref","unstructured":"Marion, J.-Y., P\u00e9choux, R.: Characterizations of polynomial complexity classes with a better intensionality. In: Proc. PPDP \u201908, pp. 79\u201388. ACM Press (2008)","DOI":"10.1145\/1389449.1389460"},{"key":"9277_CR24","unstructured":"Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Proc. FSTTCS \u201908, LIPIcs 2, pp. 304\u2013315 (2008)"},{"key":"9277_CR25","unstructured":"Moser, G.: Personal Communication (2010)"},{"key":"9277_CR26","doi-asserted-by":"crossref","unstructured":"Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In: Proc. LPAR \u201910, LNAI 6397, pp. 550\u2013564 (2010)","DOI":"10.1007\/978-3-642-16242-8_39"},{"key":"9277_CR27","doi-asserted-by":"crossref","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: A dependency pair framework for innermost complexity analysis of term rewrite systems. In: Proc. CADE \u201911, LNAI 6803, pp. 422\u2013438 (2011)","DOI":"10.1007\/978-3-642-22438-6_32"},{"key":"9277_CR28","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA \u201910, LIPIcs 6, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"9277_CR29","unstructured":"Waldmann, J.: Polynomially bounded matrix interpretations. In: Proc. RTA \u201910, LIPIcs 6, pp. 357\u2013372 (2010)"},{"key":"9277_CR30","unstructured":"Zankl, H., Korp, M.: Modular complexity analysis via relative complexity. In: Proc. RTA \u201910, LIPIcs 6, pp. 385\u2013400 (2010)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9277-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9277-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9277-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T22:43:32Z","timestamp":1745966612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9277-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,2]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["9277"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9277-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,2]]}}}