Abstract
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 language | English |
|---|---|
| Pages (from-to) | 1345-1366 |
| Number of pages | 22 |
| Journal | Journal of Logic and Computation |
| Volume | 29 |
| Issue number | 8 |
| Early online date | 31 Dec 2019 |
| DOIs | |
| Publication status | Published - 31 Dec 2019 |