Extending a Brainiac Prover to Lambda-Free Higher-Order Logic - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

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

(1) , (1, 2, 3, 4) , (5) , (6)
1
2
3
4
5
6

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-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.
Fichier principal
Vignette du fichier
conf.pdf (448.69 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02178274 , version 1 (09-07-2019)

Identifiers

  • HAL Id : hal-02178274 , version 1

Cite

Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz. Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. pp.192-210. ⟨hal-02178274⟩
48 View
254 Download

Share

Gmail Facebook Twitter LinkedIn More