Axe : SciLex
Sujet : Safely using external provers in proof assistants
Directeurs : Frédéric BLANQUI, INRIA et Guillaume BUREL, SAMOVAR
Institutions : Inria, LSV
Doctorant : Mohamed Yacine El Haddad
Début : 01/01/2018
Productions scientifiques :
- Premiers travaux
Contexte :
There exists numerous techniques to address the problem of verifying software, although none of them is sufficient on its own. The use of a proof assistant to formalize and prove the correctness of a system has now acquired a high level of maturity, with for instance CompCert, a certified optimized compiler designed and proved in Coq. However, in the perspective of their usage in the industry, such tools require a too high level of expertise for an average developer. A way to lower the skills required to benefit from these techniques would be to increase their automation. To that purpose, a cooperation of proof assistants with automated theorem provers would be of great interest. It would also be interesting to call other proof assistants whose libraries, logical system or proving environment make it easier to complete the proof.
Objectifs scientifiques
The overall goal of this PhD proposal is to design a proof environment, centered around Dedukti, that is able to call external provers to build part of the proof. It is decomposed in three tasks:
Goal 1. Interaction with external provers. The objective is to develop a way to manage calls to external provers (automated or interactive) in order to actually build a proof in Dedukti. It relies on the current work around Dedukti to turn it into a proof assistant. Although this work may appear as an engineering task, the main challenge is to warranty the consistency of the system, by making sure that at the end a correct and exhaustive proof is produced. It is expected, at the end of the thesis, to have a working environment able to call external provers and to combine part of proofs obtained by these tools. Success of the project can be judged by the use of the environment on examples with non-trivial cooperations of different provers.
Goal 2. Inputs of external provers. The Dedukti language is the λΠ-calculus modulo theory. Up to now, no prover accept this language as input, either because it is based on a weaker logic, or because it does not support rewriting rules natively. The challenge is therefore either to extend provers so that they support the λΠ-calculus modulo theory, or to design sound encodings of it into the input languages of external provers. It is expected that at least one prover, most probably ZenonModulo, will be able to understand Dedukti format, and that encodings will have been designed at least to first-order logic with or without triggers DCKP12. Success can be judged by the number of external tools able to accept input in Dedukti format without being too much burdened by the encoding if there is one.
Goal 3. Proof reconstruction. A few tools can generate Dedukti outputs. This is the case of the automated theorem provers ZenonModulo and iProverModulo. Translators also exists for proofs produced by Coq BB12b, Matita, and proof assistants of the HOL family (HOL Light, HOL 4, etc.). However, it would be unrealistic to believe that all potential external provers can be modified to produce Dedukti proofs, or roofs that can be translated to Dedukti. The challenge is to find general methods to be able to reconstruct Dedukti proofs from proof traces produced by external provers. A difficulty is that these traces contains non provable steps (e.g. Skolemization) and reasoning modulo theory. In particular, we think that there is a way to reconstruct proofs from TSTP traces. Success can be judged by the quantity of proofs that can be retrieved to Dedukti using this technique.
Perspectives :
Most of proof assistants now include a way to call external automated provers. Such provers can be considered as black boxes that have to be trusted, as for the Coq tactic why3. In another approach, traces produced by automated provers can be used to reconstruct the proof in the proof assistant. This has been introduced originally by the SledgeHammer command in Isabelle/HOL BKPU16, and it has led to several similar tools for various proof assistants (e.g. HOLyHammer for HOL Light and HOL 4 KU14.) We aim at a closer interconnection between automated theorem provers and proof assistants. First, automated provers should accept as input, possibly via encodings, the same logic as proof assistants. Second, they should produce proofs that can be directly integrated in the proof assistant. The proposal is centered around Dedukti, a proof checker for the λΠ-calculus modulo theory. This calculus is relatively simple but is expressive enough to be usable as a universal logical framework.