Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-5-1 [2011/07/12 19:26] (current)
Line 1: Line 1:
 +
 +===== Démonstration automatique I (24h, 3 ECTS) =====
 +
 +Responsables : Jean Goubault et Évelyne Contejean
 +
 +==== Intervenants prévus pour 2006-2007  ====
 +
 +   * Jean Goubault-Larrecq (4 cours = 12h)
 +   * Évelyne Contejean (4 cours = 12h)
 +
 +==== Objectifs communs aux cours C-2-5-1 et C-2-1 ====
 + Le but de ce cours de fournir aux étudiants les bases
 + nécessaires afin de pouvoir comprendre le fonctionnement de la
 + plupart des outils de démonstration automatique développés en
 + particulier dans le monde académique 
 + [[http://www.cs.miami.edu/~tptp/|(voir la page TPTP)]], et
 + éventuellement de coder eux-mêmes un tel outil.
 +  
 + Naturellement, ce cours est nécessaire pour les étudiants qui
 +poursuivraient ensuite des travaux de recherche dans le domaine de la
 +vérification, de la démonstration automatique ou de la réécriture,
 +mais aussi dans des domaines connexes comme la sécurité des systèmes
 +informatiques, les systèmes embarqués, les preuves assistées et plus
 +généralement l'utilisation des systèmes formels.
 +
 +Pour les étudiants qui souhaitent s'investir de façon plus légère, 
 +le cours est découpé en deux demi-modules. 
 +
 +==== Plan du cours ====
 +
 +   * Jean Goubault-Larrecq: Techniques de resolution.
 +
 +   * Évelyne Contejean : Logique equationnelle et completion.
 +    * logique équationelle, problème du mot, problème d'unification.
 +    * réécriture standard, modulo (cas général et AC)
 +    * confluence locale, lemme des paires critiques   
 +    * matching et unification modulo, combinaison d'algorithmes d'unification.
 +    * terminaison, introduction des ordres nécessaires RPO, LPO, KBO etc
 +    * convergence, décision du problème du mot
 +    * complétion, réécriture de preuves, critères d'élimination des paires critiques
 +    * techniques d'indexation des termes
 +Note : les premiers points seront traités si necessaire, au vu du niveau des étudiants.
 +Dans ce cas, certains des points suivants seront abordés plus succintement, ou seront 
 +supprimés. 
 +
 +
 +==== Langues du cours :  ====
 +
 +   * Jean Goubault-Larrecq fera son cours en anglais si au moins un
 +étudiant le demande, et sinon en français.
 +
 +   * Évelyne Contejean fera son cours en français, mais répondra aux questions des étudiants en anglais si ceux-ci le demande.
 +
 +   * Les langues autorisées pour l'examen sont le français et l'anglais.
 +
 +==== Supports de cours :  ====
 +   * Jean Goubault-Larrecq fournit un polycopié en anglais.
 +
 +   * Évelyne Contejean fournit un polycopié en français. Celui-ci sera traduit en anglais si des étudiants le demandent.
 +
 +==== Cours liés :  ====
 +   * Recommandé : 2-5-2
 +   * Pour la culture 2-4-1, 2-4-2, 2-7-1, 2-7-2, 2-28-1
 +
 +==== Bibliographie ====
 +L'essentiel du cours (en dehors des applications à la sécurité) se trouve dans
 +   * _A. Robinson and A. Voronkov eds_, Handbook of Automated Reasoning, vols 1 & 2, North Holland, 2001.
 +   * _Nachum Dershowitz and Jean-Pierre Jouannaud//Rewrite systems, Handbook of Theoretical Computer Science (vol. B):  Formal Models and Semantics, MIT Press, Cambridge, MA, 1991
 +
 +Sur des parties importantes du cours:
 +   * _Jean Goubault-Larrecq and Ian Mackie//Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer Academic, 1997.
 +   * //Franz Baader and Tobias Nipkow//: Term Rewriting and all that, Cambridge University Press, 1998.
 +
 +
 +==== Les années précédentes ====
 +   * [[2009-2010-C-2-5-1|Année 2009-2010]]
 +   * [[2008-2009-C-2-5-1|Année 2008-2009]]
 +   * [[2007-2008-C-2-5-1|Année 2007-2008]]
 +   * [[2006-2007-C-2-5-1|Année 2006-2007]]
 +
 +==== Équipe pédagogique ====
 +
 +|M. Bidoit|DR|CNRS|LSV|
 +|H. Comon-Lundh|PU|ENS de Cachan|LSV|
 +|E. Contejean|CR|CNRS|LRI|
 +|S. Demri|CR|CNRS|LSV|
 +|J. Goubault-Larrecq|PU|ENS de Cachan|LSV|
 +|F. Jacquemard|CR|INRIA|LSV|
 +|J.-P. Jouannaud|PU|UPS|LIX|
 +|C. Marche|CR|INRIA|LRI|
 +|R. Treinen|MC|ENS de Cachan|LSV|
 +
 +------
 +   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.HubertComonLundh, %MAINWEB%.EvelyneContejean
 +
  
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA