TY - GEN
T1 - Extending a brainiac prover to lambda-free higher-order logic
AU - Vukmirović, Petar
AU - Blanchette, Jasmin Christian
AU - Cruanes, Simon
AU - Schulz, Stephan
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85064933163&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85064933163&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-17462-0_11
DO - 10.1007/978-3-030-17462-0_11
M3 - Conference contribution
AN - SCOPUS:85064933163
SN - 9783030174613
VL - 1
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 192
EP - 210
BT - Tools and Algorithms for the Construction and Analysis of Systems
A2 - Zhang, Lijun
A2 - Vojnar, Tomáš
PB - Springer Verlag
T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
Y2 - 6 April 2019 through 11 April 2019
ER -
