English
Translating terms in first-order logic to increase automation in Coq
Recently, a proof of that all odd groups are solvable has completely formalised
within the Coq proof assistant [1].
This is quite a large development (more than 150 000 lines for 13 000 theorems)
Surprisingly, very few automation has been used in this proof. The goal of this
internship is to evaluate how this situation could be improved. One reason
that forbids the use of automatic techniques is that they are usually developed
for a weaker logic than the one of Coq. The approach follows in this internship
will be to try to understand how to get some automation by translating in
an automatic and secure way the logic of Coq into a weaker one. For this work,
we will build on previous experiments:
[2],
[3],
[4]
Français
Automatisation de preuves en Coq par traduction en logique du premier ordre.
Récemment une preuve du théorème sur la solvabilité des groupes d'ordre impair
a été complétement formalisée en Coq [1]).
Il s'agit d'un gros développement formel (plus de 150 000 lignes pour 13 000 théorèmes).
D'une façon assez surprenante cette preuve a été effectuée avec relativement peu
d'automatisation. Le but de ce stage sera de voir dans quelle mesure il serait possible
de changer cela. Un des freins à l'utilisation de méthodes automatiques est que
celles-ci s'appuient souvent sur des logiques plus faibles que celles employées par
Coq. L'approche suivie dans ce stage sera de comprendre comment récupérer
cette automatisation par application d'un traduction automatique et sure de
la logique de Coq vers une logique plus failble. Pour ce travail, on s'appuiera
sur des expériences précédentes comme
[2],
[3],
[4]
Laurent Théry