2017/06/12 by Powell, Thomas
#FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1706.03577
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ö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.