Voir la source de Initiation aux assistants de preuves (cours du LMFI)

== Introduction ==

* Utilité des assistants de preuves (vérification des mathématiques, certification de programmes, enseignement)
* Historique (Automath, LF, ...)

[http://www.cs.ru.nl/~freek/aut/ Automath] et ses [http://www.win.tue.nl/automath/ archives] : Formalisation complète du livre d'analyse de Landau E. 'Grundlagen der Analysis'.

[http://en.wikipedia.org/wiki/LF_(logical_framework) LF] and its successor [http://www.cs.cmu.edu/~fp/elf.html elf] and [http://twelf.plparty.org/wiki/Main_Page Twelf]

[http://coq.inria.fr/ CoQ] Un des systèmes les plus avancés, formalisation du théorème des 4 couleurs par G. Gonthier 

[http://www.cs.utexas.edu/users/boyer/ftp/nqthm/ Boyer-Moore's nqthm] puis [http://www.cs.utexas.edu/~moore/acl2 Moore's ACL2] : une logique au dessus du langage LISP.

[http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html Isabelle] Une meta-logique avec essentiellement deux logiques disponibles :
HOL et ZF

* 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
* Nécessite de sécuriser les données dans un [http://infosafe.fr coffre ignifugé pour data] avec serrure codée
* Puissance logique
* Risque d'incohérence

== ZFC (Mizar) ==

La théorie des ensembles est très peu utilisé pour écrire des assistances de preuves.

== La théorie des types simples de Church - HOL (Isabelle, HOL light, PhoX) ==


Définitions :

Les types simples sont construits à partir des types atomiques et de la "flêche" :
* o ou prop : le type des propositions
* <math>\omega</math> (lire omega) : le type des entiers
* <math>s \rightarrow t</math> : le type des fonctions de <math>s</math> dans <math>t</math>

Les expressions sont des <math>\lambda</math>-termes simplements typés avec une infinité de constantes 
* <math>\Rightarrow : o \rightarrow o \rightarrow o</math>
* <math>{\forall_{\!s}} : (s \rightarrow o) \rightarrow o</math> pour chaque type simple <math>s</math>
* <math>O : \omega</math>
* <math>S : \omega \rightarrow \omega</math>
* <math>\varepsilon_s : (s \rightarrow o) \rightarrow s</math> pour chaque type simple <math>s</math>
<math>{\rm L'erreur}</math>

== Les PTS (Coq) ==