| Mardi 11 septembre 2018, 14h |
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 2018, 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.
Discussion sur P et NP.
|
|
Mardi 9 octobre 2018, 14h
|
Séance de développements
DEV : Quelques problèmes indécidables sur les grammaires algébriques
DEV : 2SAT est dans P
Indécidabilité de la logique du premier ordre
|
|
Mardi 23 octobre 2018, 14h
|
Théorie de la complexité
Classe P et NP. NP-complétude. Réduction en temps polynomiale. PSPACE.
Théorème de Savitch. QBF. QBF est PSPACE-complet
Catalogue de réductions
|
|
Mardi 6 novembre 2018, 14h
|
Théorie de la complexité
DEV : 3-coloration est NP-complet
DEV : Chemin hamiltonien est NP-complet
LOGSPACE et NLOGSPACE. Problème d'accessibilité. Théorème d'Immerman-Szelepcsényi (NL= coNL).
|
|
mardi 13 novembre 2018, 14h
|
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 20 novembre 2018, 14h
|
Logique propositionnelle
Syntaxe, sémantique. Formules et circuits. Théorie, Conséquence sémantique, SAT, VALIDE. Formes normales. HORN-SAT. 2SAT. Diagramme de décision binaire.
|
|
Vendredi 30 novembre 2018, 14h
|
Séance de développements
Bijection p.r. avec réciproque p.r.
Fonction d'Ackermann n'est pas p.r.
DPLL et apprentissage de clauses. Outil en ligne : Solveur SAT en ligne.
|
| Mardi 4 décembre, 14h-16h |
Logique du premier ordre
Modèles. Syntaxe, sémantique. Variables libres/liées. Satisfiabilité, validité, conséquence sémantique. Model checking. Problème de satisfiabilité et problème de validité
Théories. Exemples de théories.
|
| Mardi 8 janvier, 14h-16h |
Séance de développements
Démonstration du théorème de compacité en logique propositionnelle comme application du théorème de Tychonoff.
La théorie des ordres denses est complète.
La théorie de Presburger est décidable. |
| Mardi 15 janvier, 10h15 |
Déduction naturelle
Présentation des règles. Règles. Exemples de preuves. Correction et complétude. Conséquences : FO est dans RE, théorème de compacité, théorème de Lowenheim-Skolem, modèles non standards.
|
| Mardi 22 janvier, 10h15 |
Séance de présentations et développements
Exemple de preuve en déduction naturelle avec présentation à la Fitch.
Démonstration de complétude de la déduction naturelle.
Calcul des séquents et résolution en premier ordre
Survol des notions.
|
| Vendredi 25 janvier, 14h |
Calcul des séquents
Exemple d'arbres de preuve.
Résolution en premier ordre
Complétude de la résolution en calcul propositionnel (développement).
Exemple de preuves. Unification. Correction. Modèle de Herbrand. Complétude.
Complétude : lemme de relèvement. Algorithme d'unification : terminaison, correction.
|