| Mardi 19 septembre 2017, 10h15 |
Machines
de Turing
Définitions machines de Turing déterministes, non-déterministes. Langages acceptés. Langages décidés. Equivalence entre machines à k-rubans et un ruban. Equivalence entre machines déterministes et non-déterministes (lemme de König). Classe R et RE. Enumérateurs.
Simulateur d'une machine de Turing déterministe
|
|
Mardi 19 septembre 2017, 13h45
|
Indécidabilité
Classes R et RE. Décidabilité et indécidabilité. Problème de l'arrêt. Machine universelle (simulation d'une machine passée en entrée). Problème de correspondance de Post. Théorème de Rice.
|
|
Mardi 10 octobre 2017, 10h15-12h15
|
NP-complétude
Rappels sur P et NP. ENS INDEP est NP-complet. Discussion autour de UNARY PRIMES et PRIMES. PRIMES est dans NP inter coNP. Discussion autour d'autres classes de complexité : L, NL, PSPACE, etc. Idée générale du théorème de Savitch.
Catalogue de réductions
|
|
Mardi 7 novembre 2017, 10h15-12h15
|
Logique propositionnelle
Quizz sur la logique propositionnelle.
Panorama.
Problème SAT. Solveur SAT en ligne.
2SAT est NL-complet.
|
|
vendredi 10 novembre 2017, 13h45-15h45
|
Théorie des fonctions récursives
Vidéo sur les fonctions primitives récursives
Exemples de fonctions récursives
D'autres exemples.
Codage de couple d'entiers. Fonctions mu-récursives.
Equivalence entre fonctions récursives primitives et le langage de programmation FOR
Equivalence entre fonctions mu-récursives partielles et le langage de programmation WHILE
Equivalence entre fonctions mu-récursives et machines de Turing.
Fonctions mu-récursives vers machines de Turing, que l'on peut alors simuler dans le simulateur
|
| mardi 14 novembre 2017, 13h30-15h30 |
Résolution
Motivation : certificats pour le problème NONSAT.
Règle de résolution. Preuves. Exemple d'arbre de réfutation.
Théorème de correction et complétude. Borne supérieure sur la taille d'une démonstration.
Borne inférieure sur la taille d'une démonstration [livre de Arora et Barak, p. 309-311].
|
| Mardi 21 novembre, 13h45-15h45 |
Logique du premier ordre
Syntaxe, sémantique. Indécidabilité du problème de satisfiabilité et du problème de validité.
Fragments décidables : fragment monadique...
|
| Vendredi 1er décembre, 13h45-15h45 |
Fragment EA. Exemple : si tout élément est d'ordre 2 dans un groupe, alors le groupe est abélien.
Déduction naturelle
Règles. Exemples de preuves. Correction.
|
| Mardi 5 décembre, 13h45-15h45 |
Complétude de la déduction naturelle.
|
| Mardi 9 janvier, 13h30-15h30 |
Calcul des séquents
Présentation des règles. Exemples d'arbres de preuve. Discussion sur la transformation d'une preuve en déduction naturelle en séquents et vice et versa. Discussion sur l'élimination de la coupure.
|
| Mardi 16 janvier, 13h30-15h30 |
Résolution en premier ordre
Exemple de preuves. Unification. Correction. Modèle de Herbrand. Complétude.
|
| Mardi 23 janvier, 10h15-12h15 |
Résolution en premier ordre
Complétude : lemme de relèvement (sur un exemple). Algorithme d'unification : terminaison, correction, exemple d'exécution.
|