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
Boyer-Moore nqthm puis ACL2
- Classification (par "sûreté" ou fondement logique)
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.