| mardi 15 novembre 2016, 10h15-12h15 |
Logique propositionnelle
Syntaxe et sémantique et problème SAT
-
Syntaxe et sémantique. Exemple avec un graphe à 3-colorier.
- Exemples de formules satisfiable, valide, de théorie. Exemple pour conséquence sémantique.
- Problème SAT : SAT solveur en ligne
Formes normales conjonctives
-
Mise en forme normale conjonctive.
- Expliquer la transformation de Tseitin.
- HORN-SAT est dans P. Exemple d'exécution de l'algorithme.
|
| mardi 22 novembre 2016, 13h30-15h30 |
Formes normales conjonctives (suite)
- 2SAT est dans P. Exemple d'exécution de l'algorithme.
|
| vendredi 25 novembre 2016, 13h30-15h30 |
Logique propositionnelle (suite)
Résolution
-
Donner un exemple d'arbre de preuve en résolution propositionnelle
- Expliquer la démonstration de la correction et complétude de la résolution
Théorème de compacité
- Démonstration du théorème de compacité
- Expliquer un des corollaires du théorème de compacité
Logique du premier ordre
Syntaxe et sémantique
Donner un ou des exemples de structures et des formules.
Variables libres/liées, substitution
Démonstration de l'indécidabilité de la validité d'une formule du premier ordre
|
| vendredi 2 décembre 2016, 13h30-15h30 |
Logique du premier ordre (suite)
Exemple de théories
Théorie des ordres denses : montrer que c'est une théorie complète
Déduction naturelle
Exemple d'une démonstration
|
| mardi 6 décembre 2016, 13h30-15h30 |
Logique du premier ordre (suite)
Déduction naturelle (suite)
Correction et complétude
Applications : théorème de compacité, Lowenheim-Skolem
Résolution
Exemple de skolémisation
|
| mardi 17 janvier 2016, 13h30-15h30 |
Logique du premier ordre (suite)
-
Donner un exemple d'arbre de preuve en résolution de bottom
-
Expliquer les modèles de Herbrand
-
Expliquer l'idée de la démonstration de la correction et complétude
-
Donner un exemple d'arbre de preuve en logique propositionnelle que l'on relève en logique du premier ordre
Calcul des séquents
-
Exemple de transformation un arbre de preuve de déduction naturelle en arbre de preuve du calcul des séquents (c'est déjà dans le poly)
-
Exemple de transformation un arbre de preuve du calcul des séquents en un arbre de preuve de déduction naturelle (le poly n'en contient pas un, j'ai besoin de vous !)
-
Expliquer comment on transforme une preuve du calcul des séquents en une preuve du calcul des séquents sans la coupure. Le must : donner un exemple pertinent avec des occurrences de la règle de coupure que l'on supprime au fur à mesure jusqu'à obtenir un arbre sans la coupure (le poly n'en contient pas un, j'ai besoin de vous !)
|