Cours de Logique à MIM à l'Ens de Lyon (1997-2002)

Cours de logique du MIM de l'ENS de Lyon (2001-2002)

Ce cours est assuré par Pierre Lescanne et Odile Millet-Botta.

Ceci se réfère à la partie du cours que j'assure. J'utilise la vidéoprojection et je n'ai fait que quelques modifications de détails par rapport aux supports de l'année précédente sauf en ce qui concerne le lambda-calcul typé.

Cette partie du cours est très orienté vers la théorie de la démonstration. Il présente la déduction naturelle et le lambda-calcul pour introduire la correspondance de Curry-Howard. Il contient cependant une petite incursion vers la théorie des modèles non classiques en introduisant les modèles de Kripke.

• Logique propositionnelle à la Hilbert (transparents tels quels et source LaTeX). 'utilise COQ avec Proof-general. Deux démonstrations sont en ligne: logique propositionnelle à la Hilbert qui est incomplète parce qu'elle contient un exercice dont voici la solution
• Déduction naturelle (transparents tels quels et source LaTeX)
• Lambda-calcul
• Généralités (transparents tels quels, Source LaTeX) plus des exercices feuille 1 (LaTeX) et feuille 2 (LaTeX).
• Confluence (transparents tels quels, Source LaTeX)
• Types (transparents tels quels, Source LaTeX) Attention, il y a un changement important par rapport à 2000, l'ajout de la preuve de normalisation forte.
• Logique classique (transparents tels quels, source LaTeX)
• Modèles de Kripke (transparents tels quels, Source LaTeX) avec un long exercice (source LaTeX) sur la complétude de la logique intuitionniste

Il y a eu un devoir (LaTeX) et un partiel (LaTeX) ainsi qu'un examen et son corrigé.

• L'utilisation de transparents

(un merci tout particulier à Laure Danthony pour sa mise en forme des «condensés«)
• logique minimale à la Hilbert (transparents tels quels et condensés (introduction, Hilbert), source LaTeX))
• logique propositionnelle naturelle (transparents tels quels et condensés, source LaTeX)
• Lambda-calcul
• Généralités (transparents tels quels, condensés, Source LaTeX)
• Confluence (transparents tels quels, condensés, Source LaTeX) un problème intéressant
• Types (transparents tels quels, condensés, Source LaTeX)
• Modèles de Kripke (transparents tels quels, condensés, Source LaTeX) avec un long exercice (source LaTeX) sur la complétude de la logique intuitionniste
• Logique classique (transparents tels quels, source LaTeX)
• L'utilisation de COQ (avec Proof-general)
• Des démonstrations COQ en cours et en ligne
• logique propositionnelle à la Hilbert
• logique naturelle propositionnelle

Un article de Jean-Yves Girard.

La logique est partout : L'ancien maire de droite à Riom qui avait été blackboulé il y a 6 ans, vient encore de se faire battre, il a commenté sa défaite en disant cette phrase qui semble avoir du sens au premier abord : « Ce n'est pas la gauche qui a gagné, c'est la droite qui a perdu «.

En 1998-99, le cours est assuré par Odile Millet-Botta et Pierre Lescanne.

• La première enseigne, dans le cadre de la logique des séquents, le calcul propositionnel et la calcul des prédicats classiques, puis la programmation logique.
• Le second présente les différents ordres de la logique. La logique du second ordre est illustrée par les règles d'induction. Ensuite, il introduit le calcul propositionnel intuitionniste minimal et étendu, les modèles de Kripke et la cohérence et la complétude de ce calcul. Cette partie du cours se termine par les logiques modales et les logiques de la connaissance.
• Afin de mettre dans le bain et d'éviter la période d'accumulation des «charrettes«, les étudiants ont eu un devoir à la maison des le premier cours. L'ensemble a été sanctionné par un partiel (partie donnée par PL) et un examen (partie donnée par PL)

.