Master Logos
Recherche pour :

Théorie de la démonstration

Code APOGÉE : MA2CE030 | 6 ECTS | Enseignant : Thierry Joly | Validation : examen
Horaires hebdomadaires : 2h CM, 2h TD | Mutualisé avec : M2 LMFI

Programme

Théorème de complétude

  • Théorème de complétude du calcul des séquents égalitaire LK par les témoins de Henkin

Calcul des séquents

  • Élimination des coupures et théorème du séquent médian dans LK
  • Théorème de Herbrand
  • Sous-calcul LJ : la logique intuitionniste et son interprétation BHK
  • Propriétés de la sous-formule et du témoin existentiel dans LJ

Déduction naturelle

  • Systèmes NK et NJ
  • Élimination des coupures de NJ
  • Propriétés de la sous-formule et du témoin existentiel dans NJ, puis dans HA (arithmétique intuitionniste)

Lambda-calcul

  • Propriétés de confluence et de standardisation
  • Représentation des fonctions récursives
  • Système T
  • Correspondance de Curry-Howard
  • Réalisabilité, normalisation forte et correction des programmes

Bibliographie

  • Cori, R. & Lascar, D. (2003). Logique mathématique, tomes 1 & 2. Paris : Dunod.
  • David, R., Nour, K. & Raffalli, C. (2004). Introduction à la logique – Théorie de la démonstration. Paris : Dunod.
  • Troelstra, A. S. & van Dalen, D. (1988). Constructivism in mathematics, Vol. I. Amsterdam : North-Holland.
  • Girard, J.-Y., Lafont, Y. & Taylor, P. (1989). Proofs and Types. Cambridge : Cambridge University Press. Disponible sur la page de P. Taylor.
  • Krivine, J.-L. (1990). Lambda-calcul : Types et Modèles. Paris : Masson. Existe en version anglaise et augmentée, disponible sur la page de l’auteur.