Evènement pour le groupe Séminaire du LaBRI


Date 2006-10-26  14:00-15:00
Titre Systèmes d'aide à la démonstration 
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 
LieuAmphi LaBRI (50) 
OrateurPierre Casteran 



Aucun document lié à cet événement.

Retour
Retour à l'index