• Cours et TD : mercredi de 14h à 18h15. À partir de 18 mars: TD de 14h à 16h, cours de 16h15 à 18h15.

• Cours : Sam van Gool

• TD : Nicolas Dumange

• Le devoir à la maison était à rendre le 8 avril avant 13h59, heure de Paris. Voici un corrigé.

• Slides: cours 1, cours 2, cours 3, cours 4, cours 5, cours 6, cours 7.

• Notes de cours:

  • Logique modale
  • Arithmétique de Presburger
  • Jeux d’Ehrenfeucht-Fraïssé

Le programme

(21 janvier et 28 janvier : pas de cours)

1. 4 février : syntaxe et sémantique de la logique propositionnelle et de la logique de premier ordre, déduction naturelle pour la logique propositionnelle. Slides

(11 février : pas de cours)

2. 18 février : déduction naturelle, tableaux, compacité et complétude de la logique propositionnelle. Slides
3. 25 février : substitution, règles de déduction pour les quantificateurs, complétude et compacité de la logique de premier ordre, théorème de Skolem. Slides

(4 mars : pas de cours)

4. 11 mars I : preuve du théorème de complétude pour la logique de premier ordre, forme normale prénexe, théorèmes de Löwenheim-Skolem, modèles et théories, axiomatisations. Slides
5. 11 mars II : théories arithmétiques, théorèmes d’incomplétude, répresentation de fonctions récursives, indécidabilité de l’arithmétique. Slides
6. 18 mars : lemme de diagonal, théorèmes de Gödel, argument de Rosser; calculs de séquents LJ et LK, propriété de disjonction de LJ. Slides
7. 25 mars : logique intuitionniste, interprétation BHK, sémantique de mondes, sémantique algébrique, algèbres de Heyting. Slides, DM
8. 1 avril : logique modale: syntaxe et sémantique, système d’Hilbert, bisimulation. Notes de cours
9. 8 avril : théorème de Hennessy-Milner, théorème de complétude de K, algèbres modales et leur représentation. Notes de cours
10. 15 avril : preuve du lemme de l’ultrafiltre et du théorème de Jónsson-Tarski; arithmétique de Presburger : axiomes, élimination de quantificateurs, réduction au cas de conjonctions de littéraux, exemples. Notes de cours
11. 22 avril : algorithme principal d’élimination de quantificateurs pour Presburger, jeux d’Ehrenfeucht-Fraïssé, exemples sur ensembles finis et ordres linéaires. Notes de cours sur Presburger, Notes de cours sur les jeux.

(29 avril : pas de cours)

• 6 mai : double TD

12. 13 mai

semaine du 18 mai : examen

Conditions de validation

La note finale sera calculée de la manière suivante :

• contrôle continu de TD : 20%
• DM : 30%
• examen : 50%

Les notes pour le contrôle continu et le DM seront maintenus en deuxième session.