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-2 [2011/07/12 19:26] (current)
Line 1: Line 1:
 +
 +===== Démonstration automatique II =====
 +
 +Responsable : Ralf Treinen
 +
 +==== Intervenants 2006-2007 ====
 +   * [[http://www.lri.fr/~contejea/|Évelyne Contejean]] (1 cours = 3 heures)
 +   * [[http://www.lsv.ens-cachan.fr/~treinen/|Ralf Treinen]] (5 cours = 15 heures)
 +   * [[http://www.lri.fr/~conchon/index.html|Sylvain Conchon]] (2 cours = 6 heures)
 +
 +
 +==== 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 ====
 +   * Évelyne Contejean : (suite) Logique du premier ordre avec égalité (3h - 28 Novembre)
 +
 +   * Ralf Treinen : Résolution de contraintes (15h - 5, 12 ,19 Décembre et Janvier 9, 16)
 +    * contraintes d'égalité sur les arbres, 
 +    * contraintes d'ordre (en particulier RPO, LPO, KBO) 
 +    * resolution de contraintes du 1er ordre en général :
 +      * élimination de quantificateurs,
 +      * techniques de décision basées sur des automates
 +    * techniques pour prouver la non-décidabilité des contraintes du premier ordre
 +
 +   * Sylvain Conchon : Procédures de décision (6h - Janvier 23 et 30)
 +    * composition de procédures de décision avec égalité : Nelson-Oppen, Shostak
 +    * briques de base : Congruence closure + extensions (listes, tableaux) 
 +    * liens avec la complétion
 +
 +==== Langue du cours ====
 +   * Évelyne Contejean fera son cours en français, mais répondra aux questions des étudiants en anglais si ceux-ci le demandent.
 +   * Sylvain Conchon fera son cours en français.
 +   * Ralf Treinen fera son cours en français ou anglais en fonction de l'auditoire.
 + 
 + Les langues autorisées pour l'examen sont le français et l'anglais. L'énoncé sera en français, mais une traduction en anglais peut être fournie si des élèves le demandent en avance.
 +
 +==== Supports de cours ====
 +   * Évelyne Contejean fournit un polycopié en français. Celui-ci sera traduit en anglais si des étudiants le demandent.
 +   * Sylvain Conchon fournit des transparents en français, une traduction en anglais peut être fournie si des étudiants le demandent.
 +   * Ralf Treinen fournit un polycopié en anglais.
 +
 +==== Pré-requis ====
 + Algèbres de termes, notions de logique du 1er ordre, savoir ce qu'est une règle d'inférence
 +
 +==== Cours liés ====
 +   * 2-5-1 Démonstration automatique 1 est recommandé.
 +   * 2-4-1 Programmation par contraintes peut être intéressant pour les applications.
 +   * 2-28-1 Automates d'arbres et applications est utile pour les techniques utilisées.
 +
 +==== Bibliographie ====
 +   * //Alan Robinson// et _[[http://www.voronkov.com/|Andrei Voronkov]]//eds, [[http://www.voronkov.com/manchester/handbook-ar/index.html|Handbook of Automated Reasoning]], vols 1 & 2, North Holland, 2001.
 +
 +   * _[[http://www.math.tau.ac.il/~nachumd/|Nachum Dershowitz]]// et //[[http://www.lix.polytechnique.fr/~jouannaud/|Jean-Pierre Jouannaud]]//: Rewrite systems. Dans Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics, MIT Press, Cambridge, MA, 1991
 +
 +   * _[[http://lat.inf.tu-dresden.de/~baader/index-en.html|Franz Baader]]// and //[[http://www4.in.tum.de/~nipkow/|Tobias Nipkow]]//: [[http://www4.in.tum.de/~nipkow/TRaAT/|Term Rewriting and all that]], Cambridge University Press, 1998.
 +
 +   * Ralf Treinen: Constraint Solving and Decision Problems of First-Order Theories of Concrete Domains, notes de cours (en anglais). [[http://www.lsv.ens-cachan.fr/~treinen/publi/constraints.ps.gz|Voir ici une version ancienne]], le document sera pour mis à jour pour ce cours.
 +
 +
 +==== Les années précédentes ====
 +   * [[2009-2010-C-2-5-2|Année 2009-2010]]
 +   * [[2008-2009-C-2-5-2|Année 2008-2009]]
 +   * [[2007-2008-C-2-5-2|Année 2007-2008]]
 +   * [[2006-2007-C-2-5-2|Année 2006-2007]]
 +
 +Équipe pédagogique
 +   * Sylvain Conchon
 +   * Évelyne Contejean
 +   * Claude Marché
 +   * Ralf Treinen
 +
 +
 +------
 +   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.EvelyneContejean, %MAINWEB%.RalfTreinen
 +
  
 
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