Traduction de HOL en Dedukti

Résumé : Les systèmes de preuve actuels (Coq, HOL, PVS, etc.) sont très utiles pour le développement des mathématiques et la vérification de programmes. Cependant, ils souffrent d'un manque d'interopérabilité qui rend difficile la réutilisation des preuves. Dedukti est un système de preuve universel basé sur le λΠ-calcul modulo qui peut exprimer des preuves venant de systèmes différents. Burel et Boespflug ont déjà travaillé sur une traduction de Coq en Dedukti. L'objectif de ce stage était de concevoir une traduction de HOL vers Dedukti. Le stage a abouti à une expression de HOL dans le λΠ-calcul modulo, ainsi qu'à un programme de traduction automatique des preuves de HOL, écrites dans le standard OpenTheory, vers Dedukti. Une partie simplifiée de l'encodage est prouvée comme étant correcte et complète. Le programme de traduction génère des fichiers qui sont vérifiés et validés par Dedukti. L'ensemble de HOL et de sa bibliothèque standard est traduit et vérifié dans Dedukti. C'est une nouvelle étape pour une meilleure interopérabilité entre les systèmes de preuve.
Type de document :
Mémoires d'étudiants -- Hal-inria+
Logique en informatique [cs.LO]. 2012
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00919871
Contributeur : Ali Assaf <>
Soumis le : mardi 17 décembre 2013 - 14:08:41
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 17 mars 2014 - 23:16:16

Fichiers

rapport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00919871, version 1

Collections

Citation

Ali Assaf. Traduction de HOL en Dedukti. Logique en informatique [cs.LO]. 2012. 〈hal-00919871〉

Partager

Métriques

Consultations de la notice

187

Téléchargements de fichiers

145