Term Orders for Optimistic Lambda-Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
TL;DR
This work introduces two higher-order term orders, $\lambda$KBO and $\lambda$LPO, tailored for the $\lambda$-superposition calculus. Each order has ground, monomorphic, and polymorphic variants that connect to their first-order counterparts via encodings, enabling properties like well-foundedness and totality to lift from first-order theory. A significant contribution is the polynomial-weight framework for nonground terms, including $\eta$-expansion effects through $\mathcal{H}$ and a type-relations $\upsilon \unrhd \tau$, which together allow practical decision procedures and optimized, interleaved algorithms inspired by Löchner. The result is a robust, scalable approach to orienting higher-order terms, with demonstrated potential for improving the effectiveness and efficiency of $\lambda$-superposition in automated theorem proving. These orders are poised to enhance Zipperposition and related systems, and the techniques may transfer to adjacent higher-order and combinatory calculi that handle extensionality axioms.
Abstract
We introduce $λ$KBO and $λ$LPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the $λ$-superposition calculus. We establish the desired properties via encodings into the familiar first-order KBO and LPO.