To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 23/11/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                        Vendredi 23 novembre, 10h30

                               --------------
                               Assia Mahboubi
                               --------------

          Projet LogiCal & Centre commun INRIA/Microsoft Research

       ==============================================================
       Preuve formelle à grande échelle et réflexion à petite échelle
       ==============================================================

En 2004, G. Gonthier a achevé la preuve formelle du théorèmes des quatre
couleurs dans l'assistant à la preuve Coq.

L'une des clefs de cette réussite est une utilisation intensive de techniques
dites de "réflexion à petite échelle", soutenues par une extension du langage
de tactiques de Coq. Cette extension, ainsi qu'une partie des bibliothèques
développées pour la preuve, sont actuellement utilisées comme point de départ
pour le projet de formalisation d'une somme substantielle de théorie des
groupes finis, dans l'équipe Composants Mathématiques du centre commun INRIA
Microsoft Research.

Il s'agit cette fois de construire une preuve formelle du théorème de
Feit-Thompson (1963), qui constitue un passage a l'échelle significatif pour
les contributions issues de la preuve du théorème des quatre couleurs.

Le but de cette expérience est de comprendre comment mener à bien le
développement de bibliothèques de mathématiques formalisées, réutilisables et
combinables. Nous tenterons d'abord de dégager les difficultés que présente la
réalisation de telles bibliothèques, puis de présenter les techniques qui se
dégagent de la preuve du théorème des quatre couleurs, et des travaux en cours
sur la théorie des groupes et en particulier le langage de tactiques
ssreflect.