Résumé | Un système d'aide à la démonstration (ou "assistant de preuve'' ) est un logiciel
permettant l'écriture et la vérification de preuves mathématiques, soit sur des théorèmes
au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de
programmes informatiques. Parmi ces logiciels, citons ACL2, Coq, HOL, Isabelle, Mizar,
etc.
Dans cet exposé, nous aborderons les thèmes suivants :
-domaines d'application
- relation entre calcul et inférence,
- théorèmes, programmes, programmes certifiés,
- degré de [non-]automaticité,
- fiabilité et lisibilité des résultats,
Les exemples seront majoritairement extraits d'un travail en cours sur les problèmes de
terminaison (avec le système Coq).
Quelques liens :
Article Wikipedia sur les assistants de preuve
http://fr.wikipedia.org/wiki/Assistant_de_preuve
Site du projet Flyspeck (preuve de la conjecture de Kepler)
http://www.math.pitt.edu/~thales/flyspeck/index.html
Site du système Coq:
http://coq.inria.fr/coq-eng.html |