Programmation et Logique

Calendrier (fichier .ics.)

Lien vers le cours de 2006 et celui de 2008.

Nouveautés

Notes finales.
Corrigé de l'examen.
Le notes de l'examen par ici
Les notes des exposés, toujours par ici.

Emploi du temps

16-09-2009 : Rappels sur la logique du premier ordre : Langages, formules. Modèles et validité. Le calcul des séquents, correction.
18-09-2009 : Le calcul des séquents : théorème de complétude. Corollaire : élimination des coupures. Machines de Turing, indecidabilité du problème de l'arrêt.
23-09-2009 : Indécidabilité de la logique du premier ordre. Logique équationnelle (et algébrique).
25-09-2009 : Décidabilité du problème du mot par représentation combinatoire de l'algèbre de Lyndenbaum. Logique multimodale, PDL (sans test) : syntaxe, sémantique. Quelques tautologies.
30-09-2009 : Caractérisation de l'étoile de Kleene comme plus petit point fixe. PDL avec test. Logique de Hoare avec Test, codage dans PDL. Théorème du modèle fini pour PDL.
2-10-2009 : Décidabilité par la propriété du modèle fini. Problèmes demi-décidables et co-demi-décidables. Séparation entre logique multimodale et PDL sans test. Séparation PDL sans test et PDL avec test.
7-10-2009 : Le plus petit point fixe, par approximations. Un example : la formule mu_x.[ ]x. Séparation entre le mu-calcul et le PDL. "Model checking" le mu-cacul : les jeux de parité. Quelques examples.
9-10-2009 : Automates sur les mots infinis. Automates de Buchi. Clôture par rapport à la réunion des langages reconnaissables. Il n'existe par un automate de Buchi déterministe reconnaissant (a+b)*a^omega. Automates à condition de Rabin et Muller. Équivalence entre les conditions d'acceptation de Buchi, Rabin et Muller. Le Théorème de McNaughton : clôture par rapport à la complémentation. Déterminisation à la Safra.
14-10-2009 : Preuve que le déterminisé d'un automate reconnaît le même langage que l'automate. Logique Monadique du II Ordre sur les nombres naturels -- MSOL(S).
17-10-2009 : Décidabilité de MSOL(S). Arithmétique de Pressburger. Automaticité. Élimination des quantificateurs. Décidabilité de l'arithmétique de Pressburger.

Exposés, lectures suggérés

Les documents sont sous acces restreint.

Attention : on travaille impérativement en binôme.

Décidabilité de quelques fragments de la logique du premier ordre :
- 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].
Décidabilité par automates :
- Automatic presentations of structures, par Khoussainov et Nerode, ici.
Logique temporelle, et logique des jeux :
- The Common Fragment of ACTL and LTL, par Mikolaj Bojanczyk, ici.
- Representation of game algebras, par Yde Venema, ici.
Une autre preuve de la décidabilité de MSOL sur les mots infinis, et le théorème de Ramsey.
- Références : [BGG, 7.1.1-7.1.17 ici] et, pour le Théorème de Ramsey, page 158 du livre [MP] ici .

D'autres possibilités : les lectures suggérées en 2006 et celles suggérées en 2008.

Attribution des exposés ici. Choix des exposés avant le mercredi 30/09/09.

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, par 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.
[MP] Le livre de Théorie de l'Ordre : une introduction, par Maurice Pouzet.
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

L'examen aura lieu le lundi 2/11, de 9h00 à 13h00, en salle 004.
Le vendredi 23/10 : les exposés, de 8h30-12h30 et 13h30 à 14h30, selon l'ordre affiché ici.
Le choix des exposé (en binôme) est à faire avant le 30/09/2009. À partir de cette date, un point par jour sera enlevé à la note d'exposé, à tous les étudiants n'ayant pas encore signalé leur choix.