A proof theoretic study of abstract termination principles
Logic in Computer Science
2019-02-25 v2 Logic
Abstract
We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in G\"{o}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 complexity of term rewrite systems.
Cite
@article{arxiv.1706.03577,
title = {A proof theoretic study of abstract termination principles},
author = {Thomas Powell},
journal= {arXiv preprint arXiv:1706.03577},
year = {2019}
}