Date: Fri, 04 Oct 1996 17:11:24 +0200 From: Marc Daumas Subject: Seminaire d'Informatique des Eleves [08/10] % Je renvoie le fichier pour les personnes qui n'utilisent pas Netscape Bonjour, Le séminaire d'informatique des élèves reprend mardi 08 octobre. Il nous sera présenté par Christine Paulin chargée de recherches au CNRS. Christine est responsable du groupe COQ au sein du LIP qui travaille sur la démonstration automatique de programmes. Les horaires du séminaire des élèves restent inchangés 13h30-14h30, amphi A. Une dernière précision suite au cafouillage de la semaine dernière: La périodicité du séminaire d'informatique des élèves reste comme l'an dernier, une fois toutes les deux semaines. Les séminaires sont annoncés par courrier électronique, dans les news (ensl.seminaire) et par affichage, à la fin de la semaine précédente. Titre ----- Mécanisation des preuves Résumé ------ Les assistants à la démonstration sont des outils informatiques dont le but est d'aider au développement de théories mathématiques. L'ordinateur assure la vérification de la correction du raisonnement et fournit des outils permettant d'écrire des preuves. Parmi les environnements les plus utilisés, on peut citer NqThm (Boyer-Moore), HOL (M. Gordon) ou PVS (Shankar). Nous présenterons la problématique du développement d'un assistant à la démonstration en nous appuyant sur le système Coq développé à l'ENS Lyon et l'INRIA Rocquencourt. -- Marc Daumas - www.ens-lyon.fr/~daumas LIP - ENS Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE Ph : (+33) 72 72 82 29 - Fx : (+33) 72 72 80 80