Les cours auront lieu les jeudis matin de 8h à 9h30, et les travaux dirigés les vendredis à 15h. Toutes les séances auront lieu à Beaulieu.
Equipe pédagogique: David Baelde et Maxime Bridoux.
Planning
- 18 janvier: tour d’horizon, calcul propositionnel (sémantique et déduction naturelle)
- 25 janvier: formes normales, problèmes SAT
- 1er février: compacité et résolution
- 8 février: complétude et stratégies de résolution
- 15 février: calcul des séquents
- 22 février: CC1 et logique constructive (§3 et version anglaise détaillée)
- (vacances)
- (vacances)
- 14 mars: logique du premier ordre
- 21 mars: substitution, calcul des séquents
- 28 mars: complétude du calcul des séquents
- 4 avril: skolémisation et théorème de Herbrand
- 11 avril: résolution
- (pas de logique la semaine du 18 avril)
- (vacances)
- 2 mai: décidabilité, théories
- (férié)
- 16 mai: examen
- 23 mai: bonus, e.g. jeux d’Ehrenfeucht-Fraïssé
Documents
Matériel de cours
- Aide mémoire sur la logique propositionnelle
- Aide mémoire sur le calcul des séquents
- Notes de cours mises à jour le 26 février
- Notes de cours détaillées en anglais on constructive logic pour les curieux
Travaux dirigés
Evaluations
- Devoir à la maison sur la logique propositionnelle
- Devoir sur table 1 corrigé
Archives 2022-23
Ressources
Si besoin, vous pouvez vous référer aux deux livres suivants, le second étant utile surtout pour la déduction naturelle, et le dernier pour le calcul des séquents:
- Logique : fondements et applications, Pierre Le Barbenchon, Sophie Pinchinat, François Schwarzentruber. Dunod.
- Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés, Karim Nour, René David, Christophe Raffalli. Dunod.
- Proofs and Types, Jean-Yves Girard, Paul Taylor, Yves Lafont.
Pour aller plus loin ou faire un pas de côté, quelques pointeurs évoqués en cours ou non:
La BD Logicomix sur la crise des fondements en mathématiques et l’origine de la logique moderne.
L’article On the Unusual Effectiveness of Logic in Computer Science pour un aperçu des rôles variés et fondamentaux de la logique en informatique.