| Date | #CM | Sujet | Exercices |
|---|---|---|---|
| 13/1 | 1 | Logique propositionnelle. Syntaxe/Sémantique | TD01 : Induction et logique propositionnelle. |
| 20/1 | 2 | Logique propositionnelle. Équivalence de formules/Substitution dans les formules/Conséquence logique d’une formule/Formes normales. | Logique propositionnelle, syntaxe et sémantique. |
| 27/1 | 3 | Logique propositionnelle. Problème SAT/Théorème de Cook 3SAT/Résolution (correction et complétude)/Compacité et applications. | Logique propositionnelle Tseitin, 2SAT, Résolution. |
| 3/2 | 4 | Logique du premier ordre. Syntaxe et sémantique des termes/Problème d'unification/Logique équationnelle. | Logique du premier ordre, termes. |
| 24/2 | 5 | Logique du premier ordre. Syntaxe et sémantique des formules/Équivalences classiques/Forme prénexe/Conséquence logique/Lemme de substitution. | Logique du premier ordre. |
| 3/3 | 6 | Logique du premier ordre. Forme universelle et forme de Skolem/Théorème de Herbrand//Théorème de compacité et applications/Théorème de Lowenheim-Skolem descendant et ascendant. | Logique du premier ordre, sémantique, skolémisation et modèles de Herbrands. |
| 10/3 | 7 | Logique du premier ordre. Problème de validité/Indécidabilité de VALID (Entscheidungsproblem)/Résolution et théorème de complétude (lemme de relèvement). | Théorème de Herbrand - Résolution en logique du premier ordre. |
| 17/3 | 8 | Logique du premier ordre. Notions de théories/Décidabilité, indécidabilité, complexité des spécifications logiques/. | Déduction naturelle, Compacité. |
| 24/3 | 9 | Logique du premier ordre. Décidabilité de la logique du premier ordre dans les structures automatiques/Arithmétique de Presburger.
transparents
|
Théories. |
| 31/3 | 10 | Théorie des modèles finis. Jeux de Ehrenfeucht-Fraïssé. | Révisions. |