Assister Automatiquement les Assistants de Preuve Avec des Traces – A3PAT

Les assistants à la preuve comme COQ bénéficient d'un noyau de vérification très sûr mais souffrent d'un manque d'automatisation. Des outils de preuve automatique performants existent mais leurs réponses ne sont pas vérifiables mécaniquement. Parmi ceux-ci, CiME est l'un des tout meilleurs sur la scène internationale pour les problèmes liés à la récriture : terminaison, complétion, etc. Notre objectif est de permettre aux assistants de preuve d'interroger des prouveurs automatiques satellites tout en préservant le haut degré de confiance qu'on leur accorde. Nous envisageons de répondre à cette forte demande par la génération de certificats à partir de traces. Cet objectif nécessite une importante étude théorique et doit se matérialiser à terme en un outil. Une première étape fondamentale est la définition d'un langage de traces capable d'exprimer la diversité de preuves de propriétés aussi complexes que terminaison ou confluence. Cette définition s'accompagne d'une modélisation des propriétés souhaitées, notamment pour garantir la complétude de certaines procédures. Il faut ensuite étudier la génération de traces pour les procédures de décision récentes, en particulier celles qui sont mises en oeuvre dans le logiciel CiME 2, développé par certains membres de notre groupe. À terme les résultats prendront forme dans une nouvelle version de CiME capable de communiquer avec COQ.