Extending a brainiac prover to lambda-free higher-order logic
     Petar Vukmirović, Jasmin Blanchette, Simon Cruanes & Stephan Schulz

Decades of work have gone into developing efficient proof calculi,
data structures, algorithms, and heuristics for first-order automatic
theorem proving. Higher-order provers lag behind in terms of
efficiency. Instead of developing a new higher-order prover from the
ground up, we propose to start with the state-of-the-art superposition
prover E and gradually enrich it with higher-order features. We
explain how to extend the prover’s data structures, algorithms, and
heuristics to $\lambda$-free higher-order logic, a formalism that supports
partial application and applied variables. Our extension outperforms
the traditional encoding and appears promising as a stepping stone
toward full higher-order logic.