Programmation et Logique

Nouveautés

• Les notes du cours sont ici.
• Un corrigé de l'examen est ici.
• Les notes de l'examen sont ici.
• Les notes des exposés sont ici.
• L'examen du cours PL aura lieu vendredi 24/10/2008, au CMI, salle 103, de 9h00 à 13h00. Documents autorisés.
• L'examen du 2006 est en ligne ici.
• Les exposés du 17/10/2008 suivront la calendrier (horaires) proposés ici.
• À partir de jeudi 2/10/2008 un point par jour sera enlevé à la note d'exposé, à tous les étudiants qui n'ont pas encore signalé leur choix d'exposé.
• Vendredi 10 octobre, à 11h00 en salle 103, aura lieu la présentation des papiers proposés pour le module communication scientifique et de stages proposés par les équipes de recherche LIF à Château Gombert.

Emploi du temps

• 10-09-2008 : Rappels de la logique du premier ordre :
  • Langages, modèles. Le calcul des sequents.
  • Théorème de completude et corollaires.

• 12-09-2008 : Decidabilité, indecidabilité :
  • Machines de Turing.
  • Indécidabilité de la logique de premier ordre.
• 17-09-2008 : Logique équationnelle (et algèbrique).

• 19-09-2008 : Logique Dynamique Propositionnelle I.
  • Logique multi-modale, PDL : syntaxe, sémantique.
  • Caractérisation de l'opérateur d'itération.

• 24-09-2008 : Logique Dynamique Propositionnelle II.
  • PDL avec l'opérateur de test.
  • Logique de Hoare et codage ce cette logique dans PDL.
  • Décidabilité par la propriété du modèle fini. Problèmes demi-décidables et co-demi-décidables.
  • Modèle fini par la méthode de filtration.
  • Pétite introduction à la théorie du plus petit point fixe.

• 26-09-2008 : Logique Dynamique Propositionnelle III et Mu-Calcul Propositionnel Modale I.
  • Fin de la preuve du modèle finis pour PDL.
  • Limites expressifs du PDL.
  • Mu-calcul : syntaxe et sémantique.
  • Pétite introduction à la théorie du plus petit point fixe.
  • Examples de formules et leur sémantique.

• 1-10-2008 : mu-calcul propositionnel modale II.
  • Le théorème fondamental du mu-calcul : satisfaction dans un état par un jeu (de parité).
  • Exemples de construction du jeu (et de satifcation ou non).
  • Preuve du théorème par la méthode des signatures.

• 3-10-2008 : Automates sur les mots infinis I.
  • Clôture sur la réunion des automates de Buchi.
  • Limites d'expressifs de automates déterministes de Buchi.
  • Conditions de (Buchi,) Rabin et Muller.

• 8-10-2008 : Automates sur les mots infinis II.
  • Équivalence entre les conditions de Buchi, Rabin et Muller.
  • Déterminisation de Safra et clôture sous la négation.

• 10-10-2008 : Decidabilité de la logique MSO sur les mots infinis.

• 15-10-2008 : Decidabilité et elimination des quantificateurs.
  • Arithmetique de Pressburger.

• 17-10-2008 : Exposés des étudiants.

Exposés, lectures suggérés

La logique dynamique propositionnelle (PDL) :

• Model Checking Propositional Dynamic Logic with All Extras, de M. Lange.

• un morecaux du survey Temporal and Modal Logic, de E. A. Emerson, pages 997--1072 de l'Handbook of Theoretical Computer Science.

• Game logic, an introduction, de Marc Pauly et Rohit Parikh.
• Game logic is strong enough for parity games, de Dietmar Berwanger.

• Les jeux de Ehrenfeucht-Fraissé et la décidabilité de la logique avec des symboles de prédicats unaires seulement. Références [GKLMSVVW, Section 2.3 ici] et [BGG, Théorème 6.2.1 ici].
• Décidabilité de la logique du premier ordre avec deux variables. Référence [BGG, Section 8.1 ici].

Attributions des exposés ici.

Références

• Le cours de Logique et Théorie du Calcul de Paul Ruet, qui se trouve ici (accès restreint).
  Chapitre sur la logique du premier ordre : 3.1, 3.2, 3.3.
  Chapitre sur les Machines de Turing : 2.1, 2.2, 2.3, 2.5, 2.6, 2.7.
• [BGG] le livre The Classical Decision Problem, de Börger, Grädel et Gurevich. Pages 18-23.
• Le livre Dynamic Logic : chapitres 3.3, 3.7, 4, 5, 6.1 et 6.2. A vous de completer la lecture des chapitres 7 et 8.
• Le chapitre 1 du livre Infinite words.
• Vos notes de cours (pour le mu-calcul, la logique monadique du II ordre, et l'arithmétique de Pressburger).
• [GKLMSVVW] le livre Finite Model Theory and Its Applications, de Grädel et al. (pour un exposé).

FAQ

• Comment le cours est évalué ?
  Voici la formule :
  (2examen + exposé)/3
  En particulier, vous (en binôme) devez préparer un exposé de 1 heure sur un sujet de votre choix entre ceux proposés ci-dessus.

Infos anciennes

• Aucune.