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.
Cite
@article{arxiv.2510.18452,
title = {Term Orders for Optimistic Lambda-Superposition},
author = {Alexander Bentkamp and Jasmin Blanchette and Matthias Hetzenberger},
journal= {arXiv preprint arXiv:2510.18452},
year = {2025}
}