Extending a brainiac prover to lambda-free higher-order logic
Keyword(s):
AbstractDecades 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.
2021 ◽
pp. 378-395
Keyword(s):
Keyword(s):
2020 ◽
Vol 34
(03)
◽
pp. 2967-2974
Keyword(s):
2009 ◽
pp. 116-130
◽
Keyword(s):