{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:38:34Z","timestamp":1740141514746,"version":"3.37.3"},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P 25781-N15"],"award-info":[{"award-number":["P 25781-N15"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,12,31]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We carry out a proof-theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees that can be defined in G\u00f6del\u2019s system T plus bar recursion. We then carry out a complexity analysis of these terms and demonstrate how this can be applied to bound the derivational height of term rewrite systems.<\/jats:p>","DOI":"10.1093\/logcom\/exz026","type":"journal-article","created":{"date-parts":[[2019,11,4]],"date-time":"2019-11-04T15:14:30Z","timestamp":1572880470000},"page":"1345-1366","source":"Crossref","is-referenced-by-count":1,"title":["A proof-theoretic study of abstract termination principles"],"prefix":"10.1093","volume":"29","author":[{"given":"Thomas","family":"Powell","sequence":"first","affiliation":[{"name":"Fachbereich Mathematik, Technische Universit\u00e4t Darmstadt, Schlossgartenstra\u00dfe 7, 64289 Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2019,12,31]]},"reference":[{"key":"2020012603564678400_ref1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-9(4:9)2013","article-title":"Polynomial path orders","volume":"9","author":"Avanzini","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"2020012603564678400_ref2","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/S0049-237X(98)80020-7","article-title":"G\u00f6del\u2019s functional (\u201cDialectica\u201d) interpretation","volume-title":"Handbook of Proof Theory","author":"Avigad","year":"1998"},{"key":"2020012603564678400_ref3","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1093\/logcom\/exv058","article-title":"An analysis of the Podelski\u2013Rybalchenko termination theorem via bar recursion","volume":"29","author":"Berardi","year":"2019","journal-title":"Journal of Logic and Computation"},{"key":"2020012603564678400_ref4","doi-asserted-by":"crossref","first-page":"1382","DOI":"10.1016\/j.apal.2015.08.002","article-title":"An intuitionistic version of Ramsey\u2019s theorem and its use in program termination","volume":"166","author":"Berardi","year":"2015","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020012603564678400_ref5","doi-asserted-by":"crossref","first-page":"2776","DOI":"10.1016\/j.tcs.2011.02.007","article-title":"Quasi-interpretations: a way to control resources","volume":"412","author":"Bonfante","year":"2011","journal-title":"Theoretical Computer Science"},{"key":"2020012603564678400_ref6","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0168-0072(94)00056-9","article-title":"Proof-theoretic analysis of termination proofs","volume":"75","author":"Buchholz","year":"1995","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020012603564678400_ref7","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"2020012603564678400_ref8","first-page":"233","article-title":"System T and the product of selection functions","volume-title":"Proceedings of Computer Science Logic (CSL \u201911)","author":"Escard\u00f3","year":"2011"},{"key":"2020012603564678400_ref9","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-60381-6_7","article-title":"Well-foundedness of term orderings","volume-title":"Conditional Term Rewriting Systems (CTRS \u201994)","author":"Ferreira","year":"1995"},{"key":"2020012603564678400_ref10","first-page":"260","article-title":"The strength of the SCT criterion","volume-title":"Proceedings of TAMC \u201917","author":"Frittaion","year":"2017"},{"key":"2020012603564678400_ref11","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-44802-0_34","article-title":"Well-founded recursive relations","volume-title":"Computer Science Logic (CSL\u201901)","author":"Goubault-Larrecq","year":"2001"},{"key":"2020012603564678400_ref12","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0304-3975(92)90289-R","article-title":"Termination proofs by multiset path orderings imply primitive recursive derivation lengths","volume":"105","author":"Hofbauer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"2020012603564678400_ref13","first-page":"105","article-title":"Ordinal analysis of bar recursion of type zero","volume":"42","author":"Howard","year":"1981","journal-title":"Compositio Mathematica"},{"key":"2020012603564678400_ref14","article-title":"Monographs in Mathematics","volume-title":"Applied Proof Theory: Proof Interpretations and Their Use in Mathematics","author":"Kohlenbach","year":"2008"},{"key":"2020012603564678400_ref15","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0049-237X(08)70845-0","article-title":"A survey of proof theory II","volume":"63","author":"Kreisel","year":"1971","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"2020012603564678400_ref16","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1215\/00294527-1715716","article-title":"Primitive recursion and the chain antichain principle","volume":"53","author":"Kreuzer","year":"2012","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2020012603564678400_ref17","first-page":"81","article-title":"The size-change principle for program termination","volume-title":"Proceedings of POPL\u201901","author":"Lee","year":"2001"},{"key":"2020012603564678400_ref18","first-page":"276","article-title":"On the computational content of termination proofs","volume-title":"Proceedings of Computability in Europe (CiE 2015)","author":"Moser","year":"2015"},{"key":"2020012603564678400_ref19","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1017\/jsl.2017.33","article-title":"A direct proof of Schwichtenberg\u2019s bar recursion closure theorem","volume":"83","author":"Oliva","year":"2018","journal-title":"Journal of Symbolic Logic"},{"key":"2020012603564678400_ref20","first-page":"32","article-title":"Transition invariants","volume-title":"Proceedings of Logic in Computer Science (LICS 2004)","author":"Podelski","year":"2004"},{"key":"2020012603564678400_ref21","doi-asserted-by":"crossref","first-page":"1727","DOI":"10.1016\/j.apal.2014.07.003","article-title":"The equivalence of bar recursion and open recursion","volume":"165","author":"Powell","year":"2014","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020012603564678400_ref22","article-title":"Well quasi-orders and the functional interpretation","volume-title":"Well Quasi-Orders in Computation, Logic, Language and Reasoning, Trends in Logic","author":"Powell","year":"2018"},{"key":"2020012603564678400_ref23","doi-asserted-by":"crossref","first-page":"325","DOI":"10.2307\/2273126","article-title":"On bar recursion of types 0 and 1","volume":"44","author":"Schwichtenberg","year":"1979","journal-title":"The Journal of Symbolic Logic"},{"article-title":"On the Constructive Content of Proofs","year":"2003","author":"Seisenberger","key":"2020012603564678400_ref24"},{"key":"2020012603564678400_ref25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/pspum\/005\/0154801","article-title":"Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics","volume-title":"Recursive Function Theory: Proc. Symposia in Pure Mathematics","author":"Spector","year":"1962"},{"key":"2020012603564678400_ref26","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","article-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"Troelstra","year":"1973"},{"key":"2020012603564678400_ref27","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1006\/jsco.1994.1059","article-title":"Complexity bounds for some finite forms of Kruskal\u2019s theorem","volume":"18","author":"Weiermann","year":"1994","journal-title":"Journal of Symbolic Computation"},{"key":"2020012603564678400_ref28","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/0304-3975(94)00135-6","article-title":"Termination proofs with lexicographic path orderings imply multiply recursive derivation","volume":"139","author":"Weiermann","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"2020012603564678400_ref29","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/s001530050107","article-title":"Bounding derivation lengths with functions from the slow growing hierarchy","volume":"37","author":"Weiermann","year":"1998","journal-title":"Archive for Mathematical Logic"},{"key":"2020012603564678400_ref30","doi-asserted-by":"crossref","first-page":"1348","DOI":"10.2307\/2586654","article-title":"How is it that infinitary methods can be applied to finitary mathematics? G\u00f6del\u2019s T: A case study","volume":"63","author":"Weiermann","year":"1998","journal-title":"Journal of Symbolic Logic"},{"key":"2020012603564678400_ref31","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.scico.2014.07.009","article-title":"A unified orderings for termination proving","volume":"111","author":"Yamada","year":"2015","journal-title":"Science of Computer Programming"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1345\/32008423\/exz026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1345\/32008423\/exz026.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,26]],"date-time":"2020-01-26T03:57:10Z","timestamp":1580011030000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/8\/1345\/5670610"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":31,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2019,12,31]]},"published-print":{"date-parts":[[2019,12,31]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz026","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2019,12]]},"published":{"date-parts":[[2019,12]]}}}