Logique

Cours de L3 à l'ENS Cachan, édition 2014-2015, par David Baelde et Hubert Comon.

Cette page contient le contenu de David Baelde: les travaux dirigés et une partie des cours. Voir la page du cours chez Hubert Comon pour ses cours, mais aussi des anciens énoncés de DM, partiels et exams.

Cours

• Intuitionistic logic (2 et 9 février): semantics, sequent calculus
• Classical sequent calculus (16 février)
• Calcul des séquents classique du premier-ordre (30 mars): voir le chapitre 1 de la thèse d'Alexis Saurin.
• Jeux de Ehrenfeucht-Fraissé (19 mai)

Travaux dirigés

• TD1 (22 janvier): logique classique, sémantique, forme clausale
• TD2 (29 janvier): logique classique, résolution
• TD3 (5 février): un exo de résolution et de l'intuitionnisme
• TD4 (12 février): intuitionnisme, Kripke et calcul des séquents
• TD5 (19 février): séquents classiques, déduction naturelle
• TD6 (5 mars): logique du premier ordre
• TD7 (12 mars): skolémisation, Herbrand
• TD8 (26 mars): unification et résolution
• TD9 (2 avril): calcul des séquents classique du premier ordre
• TD10 (9 avril): Prolog, SDL-résolution
• TD11 (16 avril): Prolog bis, NAF, déduction naturelle et séquents
• TD12 (7 mai): élimination de quantificateurs
• TD13 (21 mai): jeux d'Ehrenfeucht-Fraissé

Examens

• Partiel du 19 mars 2015: énoncé+corrigé.