A proof-theoretic study of abstract termination principles

Research output: Contribution to journalArticle

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

Cite this