2 papers
cs.LO2025
Term Orders for Optimistic Lambda-Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
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 esta…
cs.LO2025
Optimistic Higher-Order Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger +1
The -superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-or…