The Embedding Path Order for Lambda-Free Higher-Order Terms.

The embedding path order, introduced in this article, is a variant of the recursive path order (RPO) for untyped λ-free higher-order terms (also called applicative first-order terms). Unlike other higher-order variants of RPO, it is a ground-total and well-founded simplification order, making it more suitable for the superposition calculus. I formally proved the order’s theoretical properties in Isabelle/HOL and evaluated the order in a prototype based on the superposition prover Zipperposition.

Authors

• Alexander Bentkamp

Keywords

No keywords are indexed for this paper.