Initiation aux assistants de preuves (cours du LMFI)
Aller à la navigation
Aller à la recherche
Introduction
- Utilité des assistants de preuves (vérification des mathématiques, certification de programmes, enseignement)
- Historique (Automath, LF, ...)
Automath et ses archives : Formalisation complète du livre d'analyse de Landau E. 'Grundlagen der Analysis'.
LF and its successor elf and Twelf
CoQ Un des systèmes les plus avancés, formalisation du théorème des 4 couleurs par G. Gonthier
Boyer-Moore's nqthm puis Moore's ACL2 : une logique au dessus du langage LISP.
- Classification (par "sûreté" ou fondement logique)
Trois types de sécurité: systèmes à noyau (Phox, Coq, ...), systèmes basés sur les types abstraits de ML (Isabelle, ...), ou aucune sécurité (PVS, ACL2, Mizar)
Problématiques et difficultés
- Très (trop ?) différent des mathématiques informelles
- Interaction avec le calcul
- Pouvoir expressif
- Puissance logique
- Risque d'incohérence
ZFC (Mizar)
La théorie des ensembles est très peu utilisé pour écrire des assistances de preuves.