Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
Stéphane Lescuyer · 2011
Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq Dans cette thèse, nous proposons une amélioration de l'automatisation des preuves dans l'assistant de preuve Coq. Cette automatisation est obtenue en intégrant à Coq les procédures de décision pour la logique propositionnelle, l'égalité et l'arithmétique linéaire constituant le noyau du solveur SMT Alt-Ergo. Cette intégration est réalisée en utilisant la technique de preuve par réflexion, qui consiste à développer en Coq ces algorithmes et à prouver formellement leur correction de manière à les exécuter directement dans l'assistant de preuve. Comme les algorithmes formalisés en Coq sont exactement ceux utilisés dans le noyau d'Alt-Ergo, notre travail permet également d'augmenter considérablement la confiance que l'on peut avoir dans ce dernier. En particulier, il utilise un algorithme original de combinaison de l'égalité modulo une théorie, inspiré de la combinaison de Shostak et appelé CC(X), et dont la justification est relativement complexe.Notre développement Coq est utilisable sous la forme de tactiques qui permettent de valider automatiquement des formules combinant logique propositionnelle, égalité et arithmétique. Afin que ces tactiques soient le plus efficaces possibles, nous avons attaché une grande importance aux performances de notre implantation Coq, et en particulier à l'utilisation de structures de données efficaces courantes, dont nous proposons ici une bibliothèque.