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 λ -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.
CITATION STYLE
Vukmirović, P., Blanchette, J. C., Cruanes, S., & Schulz, S. (2019). Extending a brainiac prover to lambda-free higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11427 LNCS, pp. 192–210). Springer Verlag. https://doi.org/10.1007/978-3-030-17462-0_11
Mendeley helps you to discover research relevant for your work.