Initiation aux assistants de preuves (cours du LMFI)

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche

Introduction

  • Utilité des assistants de preuves (vérification des mathématiques, certification de programmes, enseignement)
  • Historique (Automath, LF, ...)
  • Classification (par "sûreté" ou fondement logique)

Problématiques et difficultés

ZFC ? (Mizar)

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

Les PTS (Coq)

Récupérée de « http://os-vps418.infomaniak.ch:1250/mediawiki/index.php?title=Initiation_aux_assistants_de_preuves_(cours_du_LMFI)&oldid=1908 »