Extending a Brainiac Prover to Lambda-Free Higher-Order Logic

                     Petar Vukmirovic
                 Jasmin Christian 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-based 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 towards full higher-order logic.