{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:32Z","timestamp":1762458632660},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_32","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"364-379","source":"Crossref","is-referenced-by-count":41,"title":["Automated Complexity Analysis Based on the Dependency Pair Method"],"prefix":"10.1007","author":[{"given":"Nao","family":"Hirokawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-51081-8_107","volume-title":"Rewriting Techniques and Applications","author":"D. Hofbauer","year":"1989","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 167\u2013177. Springer, Heidelberg (1989)"},{"issue":"1","key":"32_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(92)90289-R","volume":"105","author":"D. Hofbauer","year":"1992","unstructured":"Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS\u00a0105(1), 129\u2013140 (1992)","journal-title":"TCS"},{"key":"32_CR3","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/0304-3975(94)00135-6","volume":"139","author":"A. Weiermann","year":"1995","unstructured":"Weiermann, A.: Termination proofs for term rewriting systems with lexicographic path orderings imply multiply recursive derivation lengths. TCS\u00a0139, 355\u2013362 (1995)","journal-title":"TCS"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45127-7_10","volume-title":"Rewriting Techniques and Applications","author":"D. Hofbauer","year":"2001","unstructured":"Hofbauer, D.: Termination proofs by context-dependent interpretations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 108\u2013121. Springer, Heidelberg (2001)"},{"key":"32_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11916277_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Moser","year":"2006","unstructured":"Moser, G.: Derivational complexity of Knuth Bendix orders revisited. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 75\u201389. Springer, Heidelberg (2006)"},{"issue":"4","key":"32_CR6","first-page":"512","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. IC\u00a0205(4), 512\u2013534 (2007)","journal-title":"IC"},{"key":"32_CR7","doi-asserted-by":"publisher","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. TCS\u00a0236, 133\u2013178 (2000)","journal-title":"TCS"},{"issue":"1","key":"32_CR8","first-page":"21","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. JSC\u00a034(1), 21\u201358 (2002)","journal-title":"JSC"},{"key":"32_CR9","first-page":"474","volume":"205","author":"N. Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. IC\u00a0205, 474\u2013511 (2007)","journal-title":"IC"},{"key":"32_CR10","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 (1998)"},{"key":"32_CR11","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (2003)"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","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. JAR\u00a037(3), 155\u2013203 (2006)","journal-title":"JAR"},{"issue":"1","key":"32_CR13","doi-asserted-by":"publisher","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. JFP\u00a011(1), 33\u201353 (2001)","journal-title":"JFP"},{"key":"32_CR14","unstructured":"Geser, A.: Relative Termination. PhD thesis, Universit\u00e4t Passau (1990)"},{"key":"32_CR15","unstructured":"Steinbach, J., K\u00fchler, U.: Check your ordering \u2013 termination proofs and open problems. Technical Report SR-90-25, Universit\u00e4t Kaiserslautern (1990)"},{"issue":"4","key":"32_CR16","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR\u00a034(4), 325\u2013363 (2005)","journal-title":"JAR"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-78969-7_11","volume-title":"Functional and Logic Programming","author":"M. Avanzini","year":"2008","unstructured":"Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 130\u2013146. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:32Z","timestamp":1620016592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}