Towards Strong Higher-Order Automation for Fast Interactive Verification - Archive ouverte HAL Access content directly
Conference Papers Year :

Towards Strong Higher-Order Automation for Fast Interactive Verification

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


We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive theorem proving community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project,1 funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

Dates and versions

hal-02359588 , version 1 (12-11-2019)



Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann. Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE 2017 - 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, 2017, Göteborg, Sweden. pp.16-7, ⟨10.29007/3ngx⟩. ⟨hal-02359588⟩
21 View
0 Download



Gmail Facebook Twitter LinkedIn More