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 lambda-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.