Interoperability between proof systems using the logical framework Dedukti
Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti
Résumé
Proof systems are tools used to formally prove theorems, and in particular that software is bug-free. Proof systems provide the highest degree of confidence to prove the absence of bugs in software. However, using such tools require a high level of expertise which makes them difficult to use. The interaction with a proof system requires the user to prove and formalize many mathematical concepts. Such work is time-consuming and may require a significant amount of manpower (e.g. four-color theorem or the Hales-Kepler theorem). The diversity of proof systems has the negative consequence that these theorems (e.g. The little Fermat’s theorem) are formalized many times. This thesis investigates, both on the theoretical and the practical side, ways to translate (semi-)automatically theorems proved in one proof system to another.
Les systèmes de preuves sont des outils utilisés pour formaliser et prouver des théorèmes. Ces outils sont considérés comme le moyen le plus sûr pour montrer l’absence de bogues dans les logiciels. Cependant, l’utilisation de ces outils demandent un grand niveau d’expertise ce qui les rend difficiles à utiliser. L’interaction avec un système de preuves demande de prouver et formaliser de nombreux concepts mathématiques. Ce travail particulièrement chronophage requiert la mobilisation d’une force de travail conséquente (par exemple le théorème des quatre couleurs ou le théorème de Hales-Kepler). La diversité des systèmes de preuves induit que ces théorèmes (comme le petit théorème de Fermat) sont prouvés de nombreuses fois. Dans cette thèse, nous étudions tant sur le plan théorique que sur le plan pratique différentes façon de traduire semi-automatiquement des théorèmes prouvés depuis un système de preuve vers un autre.
Origine : Fichiers produits par l'(les) auteur(s)