Integrating Automated Theorem Provers in Proof Assistants
by Mohamed Yacine El Haddad
Thursday 9 September 2021 at 14h00
online (link to be announced)
Abstract: Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to save more time and effort for the users.
This thesis presents three contributions associated with the integration of automated provers in proof assistants.The first contribution consists of the implementation of a tactic that calls automated provers from Lambdapi by using an external platform called Why3. Usually, automated provers do not generate a complete certificate of a given formula, thus, the second contribution presented in this thesis is the reconstruction in Lambdapi of proofs generated by first-order automated provers implemented in a tool called Ekstrakto. Finally, automated provers often perform some transformations on the formula that they are trying to solve. Among these transformations, we can find Skolemization steps. The last contribution is devoted to the certification of Skolemization steps performed by the automated provers in order to have a complete reconstruction. This has been implemented in a tool called Skonverto.
Jury:
Jury members :
- Stéphane GRAHAM-LENGRAND, SRI International, USA - Reviewer
- Pascal FONTAINE, University of Liège - Reviewer
- Véronique BENZAKEN, University Paris-Saclay
- David DELAHAYE, University of Montpellier
- Cezary KALISZYK, University of Innsbruck
- Sophie TOURRET, Inria Nancy & LORIA
- Frédéric BLANQUI, Inria - Supervisor
- Guillaume BUREL, ENSIIE - Co-Supervisor