Programmation et Logique
Calendrier (fichier .ics.)
Lien vers le cours de 2006, 2008, 2009.
Nouveautés
- Les résultats de l'examen.
Emploi du temps
-
22-09-2010 : Rappels sur la logique du premier ordre :
Langages, formules. Modèles et validité. Le calcul des séquents, correction.
- 24-09-2010 : Le calcul des séquents : théorème
de complétude. Corollaire : élimination des coupures.
Machines de Turing, notion de problème, decidabilité (d'un problème).
- 29-09-2010 : Indécidabilité de du problème de l'arrêt.
Démi-décidabilité d'un problème. Décidabilité par
démi-décidabilité d'un problème et son complémentaire.
Indécidabilité de la satisfaction d'une formule du premier ordre.
Polycopié sur le Lemme de Simulation.
- 01-10-2010 : Notion de réduction d'un problème à
l'autre. Logique multimodale: syntaxe et sémantique. PDL (Logique
Dynamique Propositionnelle) sans test : syntaxe, sémantique,
quelques tautologies.
- 05-10-2010 : Bisimulations et limites expressifs de la logique
multimodale. Le théorème du modèle fini pour PDL. Décidabilité
de PDL (par la propriété du modèle fini). Preuve du théorème (I
partie).
Polycopié sur les limites expressifs de PDL.
- 07-10-2010 : Preuve du théorème du modèle fini pour PDL (II
partie). Caractérisation de l'étoile de Kleene comme plus petit
point fixe. Limites expressifs de PDL. PDL avec test. Codage
de Logique de Hoare vers PDL avec test.
- 13-10-2010 : Correction du codage de Logique de Hoare vers PDL
avec test. Limites expressifs de PDL sans test par rapport à
PDL avec test. Mu-calcul propositionnel modale, syntaxe
sémantique. La propriété "tout les calculs de s s'arrêtent" est
définissable dans le mu-calcul.
- 15-10-2010 : Automates sur les mots infinis. Automates
de Buchi. Fermeture sous la réunion. Un langage de mots
infinis, reconnaissable, mais non déterminisable.
Equivalence entre autoamtes de Buchi, de Rabin et de Muller.
- 20-10-2010 :
De Muller a Rabin : le Last Appearence Record.
Fermeture des ensembles ω-reconnaissables
sous le complément. La construction de Safra, exemples.
- 22-10-2010 : démostration du théorème de MacNaughton (
correction de la construction de Safra). Logique Monadique de II
Ordre (MSOL). Décidabilité de cette logique sur les
entiers. Ensembles de tuplet MSOL-définissables. Équivalence entre
MSOL-définissabilité et ω-reconnaissabilité.
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 compléter 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 + contrôle-continu)/3
Infos anciennes
- aucune