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 Stanislas Riou.
Planning
- 16 janvier: définitions inductives et par induction, calcul propositionnel, sémantique et déduction naturelle (TD1)
- 23 janvier: compacité et résolution (TD2)
- 30 janvier: complétude de la résolution, stratégies (TD3)
- 6 février: calcul des séquents
- 7 février: logique constructive + distribution DM
- semaine du 13 février: pas de cours, mais CC1 et TD4
- (vacances)
- (vacances)
- 27 février: normalisation de preuves (TD5)
- 6 mars: logique du premier ordre, syntaxe et sémantique (TD6)
- 13 mars: théories, décidabilité, complétude
- 20 mars: calcul des séquents et déduction naturelle
- 27 mars: complétude du calcul des séquents
- 3 avril: skolémisation et théorème de Herbrand
- (vacances)
- (vacances)
- 24 avril: résolution au premier ordre
- (pas de cours le 1er mai, dernier TD le 2 mai)
- cours décalé du 8 au 7 mai: jeux d’Ehrenfeucht-Fraïssé
- semaine du 12 mai: CC2
Documents
Matériel de cours
- Notes de cours
- Aide mémoire sur la logique propositionnelle
- Aide mémoire sur le calcul des séquents
- Devoir à la maison
- Travaux dirigés: TD1 TD2 TD3 TD4 TD5 TD6
Archives
- 2024: CC1 et CC2
- 2023: CC1 et CC2
- DM 2023 et 2024 sur la logique propositionnelle
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.
- Le roman The Maniac qui tourne principalement autour de Von Neumann, mais nous fait rencontrer Hilbert, Gödel, la naissance de l’informatique et AlphaGo.
- Le théorème de Knaster-Tarski.
- 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.