Term Orders for Optimistic Lambda-Superposition
arXiv:2510.18452
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.