| Well-foundedness of the recursive path ordering in Coq (2004) | |||||||||||||||
Abstract | |||||||||||||||
| The recursive path ordering due to Dershowitz is one of the important methods to prove termination of first-order term rewriting. The generalization to the higher-order case is due to Jouannaud and Rubio. This work is concerned with a formalization in Coq of the proof of wellfoundedness of both the first- and the higher-order version of the recursive path ordering. The proof does not rely on Kruskal’s tree theorem. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||