Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Hugo.Herbelin@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : LogiCal - 13/10/2000 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                         Vendredi 13 octobre, 10h30

                               -------------
                               Eric Deplagne
                               -------------

                                   LORIA

                     ==================================
                     L'induction comme déduction modulo
                     ==================================

                  (travail en commun avec Claude Kirchner)


    L'induction est une méthode de preuve fondamentale en mathématiques.
    Depuis l'émergence de l'informatique, elle a été etudiée et utilisée
    comme l'un des concepts fondamentaux permettant de construire
    automatiquement des preuves.

    A l'heure des logiciels sûrs, elle joue aussi un rôle fondamental dans
    les systèmes de preuve formelle. Les preuves par induction ont donc un
    rôle critique dans les assistants de preuve et les démonstrateurs
    automatiques.

    Dans les assistants de preuve, l'induction est vue comme une règle de
    déduction interactive, alors qu'en démonstration automatique elle est
    vue comme une règle de calcul appliquée automatiquement, souvent par
    réécriture.

    Dans cet exposé je présenterai comment les deux points de vue peuvent
    etre compris de manière unifiée en utilisant la déduction modulo. Nous
    offrons ainsi une nouvelle explication des méthodes d'induction basées
    sur la réécriture, parfois appelées ``induction sans induction''.

 ----------------------------------------------------------------------------
 REMARQUE: LogiCal est le nouveau nom de l'équipe Coq.