{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:23:04Z","timestamp":1740108184397,"version":"3.37.3"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T00:00:00Z","timestamp":1579132800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T00:00:00Z","timestamp":1579132800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"DFG","award":["Project KO 1737\/6-1"],"award-info":[{"award-number":["Project KO 1737\/6-1"]}]},{"name":"FWF","award":["project P-25781"],"award-info":[{"award-number":["project P-25781"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2020,5]]},"DOI":"10.1007\/s00153-019-00706-6","type":"journal-article","created":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T06:02:42Z","timestamp":1579154562000},"page":"503-516","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dependent choice as a termination principle"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2541-4678","authenticated-orcid":false,"given":"Thomas","family":"Powell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,1,16]]},"reference":[{"key":"706_CR1","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":"706_CR2","doi-asserted-by":"crossref","unstructured":"Berger, U.: A computational interpretation of open induction. In: Proceedings of LICS 2004, pp. 326\u2013334. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319627"},{"key":"706_CR3","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0168-0072(94)00056-9","volume":"75","author":"W Buchholz","year":"1995","unstructured":"Buchholz, W.: Proof-theoretic analysis of termination proofs. Ann. Pure Appl. Logic 75, 57\u201365 (1995)","journal-title":"Ann. Pure Appl. Logic"},{"key":"706_CR4","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0021089","volume":"613","author":"T Coquand","year":"1991","unstructured":"Coquand, T.: Constructive topology and combinatorics. Construct. Comput. Sci., LNCS 613, 159\u2013164 (1991)","journal-title":"Construct. Comput. Sci., LNCS"},{"issue":"3","key":"706_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term rewriting systems. Theoret. Comput. Sci. 17(3), 279\u2013301 (1982)","journal-title":"Theoret. Comput. Sci."},{"key":"706_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symbolic Comput. 3, 69\u2013116 (1987)","journal-title":"J. Symbolic Comput."},{"key":"706_CR7","doi-asserted-by":"crossref","unstructured":"Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: N.\u00a0Dershowitz (Ed.) Conditional Term Rewriting Systems (CTRS \u201994), LNCS, Vol. 968, pp. 106\u2013123","DOI":"10.1007\/3-540-60381-6_7"},{"key":"706_CR8","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq, J.: Well-founded recursive relations. In: Computer Science Logic (CSL\u201901), LNCS, Vol. 2142, pp. 484\u2013498 (2001)","DOI":"10.1007\/3-540-44802-0_34"},{"key":"706_CR9","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Automation of Reasoning. Symbolic Computation, pp. 236\u2013297. Springer (1970)"},{"key":"706_CR10","doi-asserted-by":"crossref","unstructured":"Kohlenbach, U.: Higher order reverse mathematics. In: Reverse Mathematics 2001, Lecture Notes in Logic, Vol.\u00a021, pp. 281\u2013295. ASL (2005)","DOI":"10.1017\/9781316755846.018"},{"key":"706_CR11","first-page":"518","volume":"1443","author":"PA Melli\u00e8s","year":"1998","unstructured":"Melli\u00e8s, P.A.: On a duality between Kruskal and Dershowitz theorem. Proc. ICALP, LNCS 1443, 518\u2013529 (1998)","journal-title":"Proc. ICALP, LNCS"},{"key":"706_CR12","doi-asserted-by":"crossref","unstructured":"Moser, G., Powell, T.: On the computational content of termination proofs. In: Proceedings of Computability in Europe (CiE 2015), LNCS, Vol. 9136, pp. 276\u2013285 (2015)","DOI":"10.1007\/978-3-319-20028-6_28"},{"key":"706_CR13","unstructured":"Powell, T.: On bar recursive interpretations of analysis. Ph.D. thesis, Queen Mary University of London (2013)"},{"issue":"11","key":"706_CR14","doi-asserted-by":"publisher","first-page":"1727","DOI":"10.1016\/j.apal.2014.07.003","volume":"165","author":"T Powell","year":"2014","unstructured":"Powell, T.: The equivalence of bar recursion and open recursion. Ann. Pure Appl. Logic 165(11), 1727\u20131754 (2014)","journal-title":"Ann. Pure Appl. Logic"},{"key":"706_CR15","doi-asserted-by":"crossref","unstructured":"Powell, T.: A proof theoretic study of abstract termination principles (2019). To appear in: Journal of Logic and Computation","DOI":"10.1093\/logcom\/exz026"},{"key":"706_CR16","doi-asserted-by":"crossref","unstructured":"Powell, T.: Well quasi-orders and the functional interpretation. In: Schuster, P., Seisenberger, M., Weiermann, A. (eds.) Well-Quasi Orders in Computation, Logic, Language and Reasoning. Trends in Logic, vol. 53. Springer, pp. 221\u2013269 (2020)","DOI":"10.1007\/978-3-030-30229-0_9"},{"key":"706_CR17","unstructured":"Seisenberger, M.: On the constructive content of proofs. Ph.D. thesis, Ludwig Maximilians Universit\u00e4t M\u00fcnchen (2003)"},{"key":"706_CR18","doi-asserted-by":"crossref","unstructured":"Sternagel, C.: A mechanized proof of Higman\u2019s lemma by open induction. In: Schuster, P., Seisenberger, M., Weiermann, A. (eds.) Well-Quasi Orders in Computation, Logic, Language and Reasoning. Trends in Logic, vol. 53. Springer, pp. 339\u2013350 (2020)","DOI":"10.1007\/978-3-030-30229-0_12"},{"key":"706_CR19","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"AS Troelstra","year":"1973","unstructured":"Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973)"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-019-00706-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-019-00706-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-019-00706-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,15]],"date-time":"2021-01-15T02:14:27Z","timestamp":1610676867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-019-00706-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,16]]},"references-count":19,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2020,5]]}},"alternative-id":["706"],"URL":"https:\/\/doi.org\/10.1007\/s00153-019-00706-6","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2020,1,16]]},"assertion":[{"value":"2 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 January 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}