{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:26:24Z","timestamp":1743063984694,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319200279"},{"type":"electronic","value":"9783319200286"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-20028-6_28","type":"book-chapter","created":{"date-parts":[[2015,6,19]],"date-time":"2015-06-19T10:07:37Z","timestamp":1434708457000},"page":"276-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Computational Content of Termination Proofs"],"prefix":"10.1007","author":[{"given":"Georg","family":"Moser","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Powell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,20]]},"reference":[{"key":"28_CR1","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 105, 129\u2013140 (1992)","journal-title":"TCS"},{"key":"28_CR2","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 ordering imply multiply recursive derivation lengths. TCS 139, 355\u2013362 (1995)","journal-title":"TCS"},{"key":"28_CR3","first-page":"57","volume":"75","author":"W Buchholz","year":"1995","unstructured":"Buchholz, W.: Proof-theoretic analysis of termination proofs. APAL 75, 57\u201365 (1995)","journal-title":"APAL"},{"doi-asserted-by":"crossref","unstructured":"Parsons, C.: On a number theoretic choice schema and its relation to induction. In: Proceedings of the Intuitionism and Proof Theory, pp. 459\u2013473 (1970)","key":"28_CR4","DOI":"10.1016\/S0049-237X(08)70771-7"},{"key":"28_CR5","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":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-44881-0_21","volume-title":"Rewriting Techniques and Applications","author":"G Moser","year":"2003","unstructured":"Moser, G., Weiermann, A.: Relating derivation lengths with the slow-growing hierarchy directly. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 296\u2013310. Springer, Heidelberg (2003)"},{"key":"28_CR7","first-page":"171","volume-title":"Proof Theory","author":"EA Cichon","year":"1992","unstructured":"Cichon, E.A.: Termination orderings and complexity characterisations. In: Aczel, P., Simmons, H., Wainer, S.S. (eds.) Proof Theory, pp. 171\u2013193. Cambridge University Press, Cambridge (1992)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BFb0055776","volume-title":"Mathematical Foundations of Computer Science 1998","author":"H Touzet","year":"1998","unstructured":"Touzet, H.: Encoding the hydra battle as a rewrite system. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol. 1450, p. 267. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Moser, G.: KBOs, ordinals, subrecursive hierarchies and all that. JLC (2015, to appear)","key":"28_CR9","DOI":"10.1093\/logcom\/exu072"},{"doi-asserted-by":"crossref","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with dickson\u2019s lemma. In: Proceedings of the 26th LICS, pp. 269\u2013278. IEEE (2011)","key":"28_CR10","DOI":"10.1109\/LICS.2011.39"},{"unstructured":"Berardi, S., Oliva, P., Steila, S.: Proving termination with transition invariants of height $$\\omega $$. In: Proceedings of the 15th ICTCS, pp. 237\u2013240 (2014)","key":"28_CR11"},{"key":"28_CR12","volume-title":"Term Rewriting Systems. Cambridge Tracks in Theoretical Computer Science","author":"Terese","year":"2003","unstructured":"Terese, : Term Rewriting Systems. Cambridge Tracks in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-60381-6_7","volume-title":"Conditional and Typed Rewriting Systems","author":"MCF Ferreira","year":"1995","unstructured":"Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol. 968, pp. 106\u2013123. Springer, Heidelberg (1995)"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/3-540-44802-0_34","volume-title":"Computer Science Logic","author":"J Goubault-Larrecq","year":"2001","unstructured":"Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, p. 484. Springer, Heidelberg (2001)"},{"key":"28_CR15","first-page":"1348","volume":"63","author":"A Weiermann","year":"1998","unstructured":"Weiermann, A.: How is it that infinitary methods can be applied to finitary mathematics? G\u00f6del\u2019s T: a case study. JSL 63, 1348\u20131370 (1998)","journal-title":"JSL"},{"key":"28_CR16","first-page":"93","volume":"95","author":"T Arai","year":"1998","unstructured":"Arai, T.: Some results on cut-elimination, provable well-orderings, induction, and reflection. APAL 95, 93\u2013184 (1998)","journal-title":"APAL"},{"key":"28_CR17","first-page":"199","volume":"83","author":"EA Cichon","year":"1997","unstructured":"Cichon, E.A., Weiermann, A.: Term rewriting theory for the primitive recursive functions. APAL 83, 199\u2013223 (1997)","journal-title":"APAL"}],"container-title":["Lecture Notes in Computer Science","Evolving Computability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20028-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T01:36:11Z","timestamp":1676943371000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20028-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319200279","9783319200286"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20028-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"20 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}