Abstract
We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.
Cite
CITATION STYLE
Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A lambda-free higher-order recursive path order. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10203 LNCS, pp. 461–479). Springer Verlag. https://doi.org/10.1007/978-3-662-54458-7_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
