Skip to Main content Skip to Navigation
Conference papers

Towards Strong Higher-Order Automation for Fast Interactive Verification

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 12, 2019 - 2:36:57 PM
Last modification on : Tuesday, December 10, 2019 - 4:48:47 PM

Links full text




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⟩



Record views