{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:11Z","timestamp":1740123311852,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T00:00:00Z","timestamp":1481932800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T00:00:00Z","timestamp":1481932800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["GI 274\/6-1"],"award-info":[{"award-number":["GI 274\/6-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10817-016-9397-x","type":"journal-article","created":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T13:39:55Z","timestamp":1481981995000},"page":"121-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Lower Bounds for Runtime Complexity of Term Rewriting"],"prefix":"10.1007","volume":"59","author":[{"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jera","family":"Hensel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cornelius","family":"Aschermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Str\u00f6der","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,12,17]]},"reference":[{"key":"9397_CR1","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3), 22 (2013)","DOI":"10.1145\/2499937.2499943"},{"key":"9397_CR2","unstructured":"AProVE. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/lowerbounds-journal\/"},{"key":"9397_CR3","unstructured":"Avanzini, M., Moser, G.: A combination framework for complexity. In: Proceedings of RTA\u00a0\u201913. LIPIcs 21, pp. 55\u201370 (2013)"},{"key":"9397_CR4","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schaper, M.: $${\\sf TcT}$$: Tyrolean complexity tool. In: Proceedings of TACAS\u00a0\u201916. LNCS 9636, pp. 407\u2013423 (2016)","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"9397_CR5","doi-asserted-by":"publisher","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 (1998)"},{"key":"9397_CR6","volume-title":"A Computational Logic","author":"Robert S Boyer","year":"1979","unstructured":"Boyer, Robert S., Moore, J.S.: A Computational Logic. Academic Press, Cambridge (1979)"},{"key":"9397_CR7","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS\u00a0\u201908. LNCS 4963, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9397_CR8","doi-asserted-by":"crossref","unstructured":"Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: Proceedings of IJCAR\u00a0\u201912. LNAI 7364, pp. 225\u2013240 (2012)","DOI":"10.1007\/978-3-642-31365-3_19"},{"key":"9397_CR9","unstructured":"Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Str\u00f6der, T.: Inferring lower bounds for runtime complexity. In: Proceedings of RTA\u00a0\u201915. LIPIcs 36, pp. 334\u2013349 (2015)"},{"key":"9397_CR10","doi-asserted-by":"crossref","unstructured":"Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Proceedings of IJCAR\u00a0\u201916. LNAI 9706, pp. 550\u2013567 (2016)","DOI":"10.1007\/978-3-319-40229-1_37"},{"issue":"2","key":"9397_CR11","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10817-010-9215-9","volume":"47","author":"C Fuhs","year":"2011","unstructured":"Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dependency pairs and inductive theorem proving. J. Autom. Reason. 47(2), 133\u2013160 (2011)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9397_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s10817-005-9024-8","volume":"34","author":"A Geser","year":"2005","unstructured":"Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. J. Autom. Reason. 34(4), 365\u2013385 (2005)","journal-title":"J. Autom. Reason."},{"key":"9397_CR13","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proceedings of FroCoS\u00a0\u201905. LNAI 3717, pp. 216\u2013231 (2005)","DOI":"10.1007\/11559306_12"},{"key":"9397_CR14","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 (2011)","DOI":"10.1145\/1890028.1890030"},{"key":"9397_CR15","doi-asserted-by":"crossref","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F.,Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P.,Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with $${{\\sf AProVE}}$$. J. Autom. Reason (to appear). Preliminary version appeared in Proceedings of IJCAR\u00a0\u201914. LNAI 8562, pp. 184\u2013191 (2014)","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"9397_CR16","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proceedings of IJCAR\u00a0\u201908. LNAI 5195, pp. 364\u2013379 (2008)","DOI":"10.1007\/978-3-540-71070-7_32"},{"key":"9397_CR17","doi-asserted-by":"crossref","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA\u00a0\u201989. LNCS 355, pp. 167\u2013177 (1989)","DOI":"10.1007\/3-540-51081-8_107"},{"key":"9397_CR18","unstructured":"Hofbauer, D., Waldmann, J.: Constructing lower bounds on the derivational complexity of rewrite systems. Slides of a Talk at the 2nd Workshop on Proof Theory and Rewriting. http:\/\/www.imn.htwk-leipzig.de\/~waldmann\/talk\/10\/pr\/main.pdf (2010)"},{"key":"9397_CR19","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Moser, G.: Amortised resource analysis and typed polynomial interpretations. In: Proceedings of RTA-TLCA\u00a0\u201914. LNCS 8560, pp. 272\u2013286 (2014)","DOI":"10.1007\/978-3-319-08918-8_19"},{"issue":"2","key":"9397_CR20","doi-asserted-by":"publisher","first-page":"219","DOI":"10.2307\/2269811","volume":"31","author":"PK Hooper","year":"1966","unstructured":"Hooper, P.K.: The undecidability of the Turing machine immortality problem. J. Symb. Log. 31(2), 219\u2013234 (1966)","journal-title":"J. Symb. Log."},{"issue":"203","key":"9397_CR21","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1090\/S0025-5718-1993-1197512-7","volume":"61","author":"D Knuth","year":"1993","unstructured":"Knuth, D.: Johann Faulhaber and sums of powers. Math. Comput. 61(203), 277\u2013294 (1993)","journal-title":"Math. Comput."},{"key":"9397_CR22","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Basic syntactic mutation. In: Proceedings of CADE\u00a0\u201918. LNAI 2392, pp. 471\u2013485 (2002)","DOI":"10.1007\/3-540-45620-1_37"},{"issue":"3","key":"9397_CR23","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"9397_CR24","doi-asserted-by":"crossref","unstructured":"Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. Log. Methods Comput. Sci. 7(3:01), 1\u201338 (2011)","DOI":"10.2168\/LMCS-7(3:1)2011"},{"issue":"1","key":"9397_CR25","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s10817-013-9277-6","volume":"51","author":"L Noschinski","year":"2013","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27\u201356 (2013)","journal-title":"J. Autom. Reason."},{"key":"9397_CR26","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of RTA\u00a0\u201910. LIPIcs 6, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"issue":"2\u20133","key":"9397_CR27","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/j.tcs.2008.05.013","volume":"403","author":"\u00c9 Payet","year":"2008","unstructured":"Payet, \u00c9.: Loop detection in term rewriting using the eliminating unfoldings. Theor. Comput. Sci. 403(2\u20133), 307\u2013327 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"9397_CR28","unstructured":"Termination Comp. http:\/\/termination-portal.org\/wiki\/Termination_Competition"},{"key":"9397_CR29","doi-asserted-by":"crossref","unstructured":"Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of RTA\u00a0\u201904. LNCS 3091, pp. 85\u201394 (2004)","DOI":"10.1007\/978-3-540-25979-4_6"},{"key":"9397_CR30","doi-asserted-by":"crossref","unstructured":"Waldmann, J.: Automatic termination. In: Proceedings of RTA\u00a0\u201909. LNCS 5595, pp. 1\u201316 (2009)","DOI":"10.1007\/978-3-642-02348-4_1"},{"key":"9397_CR31","doi-asserted-by":"crossref","unstructured":"Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A.: Finding and certifying loops. In: Proceedings of SOFSEM\u00a0\u201910. LNCS 5901, pp. 755\u2013766 (2010)","DOI":"10.1007\/978-3-642-11266-9_63"},{"key":"9397_CR32","doi-asserted-by":"crossref","unstructured":"Zankl, H., Korp, M.: Modular complexity analysis for term rewriting. Log. Methods Comput. Sci. 10(1:19), 1\u201333 (2014)","DOI":"10.2168\/LMCS-10(1:19)2014"},{"issue":"1","key":"9397_CR33","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symbol. Comput. 17(1), 23\u201350 (1994)","journal-title":"J. Symbol. Comput."},{"issue":"2","key":"9397_CR34","doi-asserted-by":"publisher","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\/article\/10.1007\/s10817-016-9397-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9397-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9397-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,17]],"date-time":"2022-07-17T16:14:16Z","timestamp":1658074456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9397-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,17]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9397"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9397-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,12,17]]},"assertion":[{"value":"25 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 November 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}