A Lambda-Free Higher-Order Recursive Path Order

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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-01592189
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 6:44:57 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Thursday, December 28, 2017 - 12:16:37 PM

File

BlanchetteWaldmannWandFoSSaCS....
Files produced by the author(s)

Identifiers

Citation

Jasmin Blanchette, Uwe Waldmann, Daniel Wand. A Lambda-Free Higher-Order Recursive Path Order. Javier Esparza and Andrzej S. Murawski. Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. Springer, 10203, pp.461-479, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-662-54458-7_27〉. 〈hal-01592189〉

Share

Metrics

Record views

135

Files downloads

43