Mercredi 17/07/2013, à partir de 10h30, en salle Byron Blanc.
Orateur : Antoine Grospellier.
Titre : Automatisation de preuves en coq par traduction en logique du premier ordre.
Résumé :
J’ai essayé de comprendre le fonctionnement des logiciels why (et sa tactique coq) et isabelle (principalement sa fonction sledgehammer). Maintenant je tente de modifier why pour prouver un maximum de lemmes de la bibliothèque de ssreflect automatiquement.
