Dedukti : un vérificateur de preuves universel
Résumé
- Dedukti est un veri cateur de type pour -calcul modulo.
- Le -calcul modulo est une extension du -calcul avec des types dépendants et une relation de conversion étendue par des règles
de reecriture.
- Dedukti est capable de verifi er les preuves provenant de prouveurs de théorèmes (Zenon, iProver) et d'assistants de preuves
(Coq, HOL, Focalize).
- On montre a travers plusieurs exemples que l'utilisation de la rééecriture caractéristique du -calcul modulo permet d'obtenir des preuves plus petites et plus rapides à vérifi er.
Origine : Fichiers produits par l'(les) auteur(s)