Initiation aux assistants de preuves (cours du LMFI)

De Wiki du LAMA (UMR 5127)
Aller à : navigation, rechercher

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}

Les PTS (Coq)