Le cours vise l'étude de la déduction naturelle pour la logique classique du premier ordre et de ses sous-systèmes. Nous allons étudier en particulier le résultat de l'élimination des coupures et ses principales applications. Le cours se poursuivra ensuite par une discussion sur la constructivité pour le cas intuitionniste et par des considérations sur la constructivité pour le cas classique.
Références bibliographiques
- David, R., Nour, K., et Raffalli, C. Introduction à la logique : Théorie de la démonstration. Dunod, Paris. 2001.
- Girard, J., Lafont, Y., et Taylor, P. Proofs and Types. Cambridge University Press, Cambridge. 1989.
- Prawitz, D. Natural Deduction. Almquist et Wiksell, Stockholm. 1965.
Jour et heure du cours : mercredi, 17h - 19h
Lieu du cours : Salle Halbwachs (17 Rue de la Sorbonne, escalier C, 1er étage)
- Enseignant éditeur: Genco Francesco
