Towards Strong Higher-Order Automation for Fast Interactive Verification

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