Portal de Periódicos da CAPES

Extending a brainiac prover to lambda-free higher-order logic

2021; Springer Science+Business Media; Volume: 24; Issue: 1 Linguagem: Inglês

10.1007/s10009-021-00639-7

1433-2787

Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz,

Formal Methods in Verification

Abstract 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.