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