3 papers
cs.LO2026
Tao's Equational Proof Challenge Accepted (Technical Report)
Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover.…
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…