Programmation et Logique

Nouveautés

• Un corrigé de l'examen ici.
• Évaluation des exposés ici.
• Évaluation de l'examen ici.
• Décachetage et discussion des copies à partir de jeudi 2 novembre.

Emploi du temps

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

• 22-09-2006 : Decidabilité, indecidabilité :
  • Machines de Turing. Indcidabilité de la logique de premier ordre.
  • Logique équationnelle

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

• 29-09-2006 : Logique Dynamique Propositionnelle II.
  • Axiomatisation du 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.

• 4-10-2006 : mu-calcul propositionnel modale I.
  • Syntaxe et sémantique.
  • Pétite introduction à la théorie du plus petit point fixe.

• 6-10-2006 : mu-calcul propositionnel modale II.
  • Le théoreme fondamental du mu-calcul : satisfaction dans un état et jeux de parité.

• 13-10-2006 : Automates sur les mots infinis.
  • Cloture sur le runion.
  • Cloture sous la negation : conditions de Buchi, Rabin et Muller.
  • Determinization de Safra.

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

• 20-10-2006 : Decidabilité et elimination des quantificateurs.
  • Arithmetique de Pressburger.

• 22-10-2006 : Exposés des étudiants.

Exposéz, lectures suggérés

• Le problème de la correspondance de Post, indecidabilité du problème du mot pour le monoïdes de présentation finie.
  Référence : le livre de Sipser Introduction to the Theory of Computation.
• Un article du livre Automata Logics and Infinite Games
• Algebraic and model theoretic techniques in Modal Logics.
• Game logic is strong enough for parity games.
• On the variable hierarchy of the modal mu-calculus.
• ...

Références

• Le cours de logique et complexité du MasterII MDFI, qui se trouve ici.
  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.
• Pages 18-23 du livre The Classical Decision Problem.
• 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).

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.