Cours logiques non classiques, Master Informatique Fondamentale, année 2016-2017

Infos

• Un deuxième possible sujet de Master, autour des ordinaux de clôture du mu-calcul.
• Un possible sujet de Master, sur la théorie de la correspondance pour la logique modale monotone.
• Début du cours : le vendredi 18 novembre 2016

Emploi du temps

1. Vendredi 18/11 : Logique propositionnelle modale K : syntaxe. Sémantique : frames et modèles. Équivalences élémentaires entre formules. Bisimulations, théorème de Van Benthem.
2. Vendredi 25/11 : théorème de Van Benthem (fin). Théorème du modèle arborescente, théorème du modèle fini. Approche algébrique à la logique propositionnelle : algèbres de Boole et algèbres modales. Filtres et ultrafiltres, théorème de Stone pour les algèbres de Boole.
3. Vendredi 9/12 : Extension du théorème de Stone aux algèbres modales. Axiomatisation de la logique modale K, correction par rapport aux tautologies. Algèbre de Lyndenbaum de la logique K, théorème complétude pour K.
4. Vendredi 16/12 : Logiques modales. Axiomes T, 4, 5, D0 et D1. (Correction et) Complètude de la logique K4. Notion de formule du premier ordre correspondante à une formule modale. Éléments de la théorie de la correspondance, énoncé du Théorème de Sahlqvist.
5. Vendredi 6/1 : Logiques du calcul. PDL (logique propositionnelle dynamique). Théorie du plus petit (et du plus grand) point-fixe. Théorème de Tarski-Knaster, théorème de Tarski-Knaster-Park.
6. Vendredi 13/1 : mu-calcul propositionnel modal. Filtration pour PDL, pouvoir expressif du nu-calcul. Jeux de parité et formule du mu-calcul pour lénsemble de positions gagnantes dans jeu de parité.
7. Vendredi 20/1 : ???

Exercices

1. Cours du vendredi 18/11.
2. Cours du vendredi 25/11.
3. Cours du vendredi 9/12. Aussi, un exercice qui vous guide à la preuve du Lemme de l'ultrafiltre.
4. Cours du vendredi 16/12.
5. Cours du vendredi 6/01.
6. Cours du vendredi 13/01.

Contenu (envisagé) du cours

• Logique propositionnelle modale K, syntaxe.
• Sémantique : frames et modèles. Équivalences élémentaires de formules. Bisimulations, théorème de Van Benthem.
• Approche algébrique à la logique propositionnelle
• Complètude et dualité de Stone
• Théorème du modèle fini, décidabilité
• Variétés de logiques modales
• Théorie de la correspondance, fragment de Salqvist
• Canonicité
• Filtrations
• Logiques du calcul : LTL, PDL, CTL, mu-calcul propositionnel
• Logique (propositionnelle) intuitionniste
• Frames et modèles
• Plongement de la LI dans la logique modale S4, théorème de Esakia
• Systèmes de preuve pour la logique intuitionniste
• Logique intuitionniste et lambda-calculs

Références

• Marcus Kracht. Tools and Techniques in Modal Logic, Volume 142 of Studies in logic and the foundation of mathematics. ELSEVIER 1999.
• Robert Goldblatt, Logics of Time and Computation. CSLI Lecture Notes No. 7, 1992.
• Patrick Blackburn, Maarten de Rijke, Yde Venema. Modal Logic, Cambridge Tracts in Theoretical Computer Science, 2002.
• Coling Stirling. Modal and Temporal Properties of Processes Springer (Texts in Computer Science), 2001.

Calcul de la note finale