A proof-theoretic study of abstract termination principles

Research output: Contribution to journalArticlepeer-review


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ödel’s 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.
Original languageEnglish
Pages (from-to)1345-1366
Number of pages22
JournalJournal of Logic and Computation
Issue number8
Early online date31 Dec 2019
Publication statusPublished - 31 Dec 2019


Dive into the research topics of 'A proof-theoretic study of abstract termination principles'. Together they form a unique fingerprint.

Cite this