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, ...)

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.

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 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
• $\omega$ (lire omega) : le type des entiers
• $s\rightarrow t$ : le type des fonctions de $s$ dans $t$

Les expressions sont des $\lambda$-termes simplements typés avec une infinité de constantes

• $\Rightarrow :o\rightarrow o\rightarrow o$
• ${\forall _{\!s}}:(s\rightarrow o)\rightarrow o$ pour chaque type simple $s$
• $O:\omega$
• $S:\omega \rightarrow \omega$
• $\varepsilon _{s}:(s\rightarrow o)\rightarrow s$ pour chaque type simple $s$

${\rm {L'erreur}}$