Optimistic Higher-Order Superposition

Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger +1

The $\hat{I}»$-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…