Vous trouverez ici le matériel produit par David Baelde. Pour le matériel des autres enseignants, voir sur leurs pages respectives: Hubert Comon, Guillaume Genestier.
Notes de cours
- 14 février: logique intuitionniste, déduction naturelle et sémantique de Kripke (PDF)
- 21 février: normalisation de preuves pour NJ0 (PDF) et calcul des séquents intuitionniste (PDF)
- 28 février: calcul des séquents classique, complétude, version unilatère, etc. (PDF)
- 14 mars: calcul des prédicats, syntaxe et sémantique (PDF)
- 21 mars: substitutions, α-renommage, modèles non-standards de l'arithmétique élémentaire (PDF)
- 28 mars: calcul des séquents LK1 (PDF)
- 4 avril: fin LK1, et quelques pas vers la forme clausale (PDF)
Devoir à la maison
Un devoir sur les preuves infinitaires pour les algèbres de Kleene est à rendre le 3 avril. Voici la solution partiellement rédigée, avec errata.
Partiel
Le sujet et le corrigé partiellement rédigé du partiel 2019.