Tags:Higher-order term rewriting, Recursive path ordering and Termination
Abstract:
The higher-order recursive path ordering is one of the oldest, but still very effective, methods to prove termination of higher-order TRSs. A limitation of this ordering is that it is not transitive (and its transitive closure is not computable). We will present a transitive variation of HORPO. Unlike previous HORPO definitions, this method can be used directly on terms in curried notation.