THE EMBEDDING PATH ORDER FOR LAMBDA-FREE HIGHER-ORDER TERMS

JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS(2021)

引用 0|浏览3
暂无评分
摘要
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.
更多
查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要