MATH0980 : contenu algorithmique des démonstrations mathématiques

Ce wiki est un complément pour le cours du Master deuxième année intitulé "contenu algorithmique des démonstrations mathématiques". Le cours est donné par Karim Nour et Pierre Hyvernat à l'université Claude Bernard, à Lyon...

Nous encourageons tous les étudiants à y participer en l'augmentant au fur et à mesure de l'avancement du cours.

Pour pouvoir modifier les pages, inscrivez-vous pour obtenir un login et mot de passe. (S'il vous plaît, utilisez votre vrai nom...)

Allez regarder ici pour vous familiariser avec les wikis.

Vous pouvez également utiliser la page de discussion pour ... discuter (ou poser des questions).

Exercice : créez-vous un compte et essayez de modifier cette page (correction de fôtes d'aurtograffe, rajout de détails, mise en page, ...)

Details techniques / administratifs

Nouvelles

Les nouvelles importantes pour le cours (les plus récentes en haut).

Rq : pour mettre la date dans le wiki, il suffit de mettre "~~~~".

• Hyvernat 23 janvier 2008 à 09:23 (CET) : le cours a disparu, mais il revient ! Nous commencerons donc avec une semaine de retard...
• Hyvernat 4 janvier 2008 à 14:16 (CET) : création du wiki.

Plan (provisoire) du cours

• Séance 1 : 17 janvier (KN) Présentation du cours ; déduction naturelle et traduction de Gödel.

• Séance 2 : 24 janvier (KN) Sémantiques pour les logiques classiques et intuitionniste.

• Séance 3 : 31 janvier (KN) Calcul des séquents et élimination des coupures.

• Séance 4 : 7 février (PH) Introduction au lambda-calcul : Church-Rosser.

• Séance 5 : 14 février (PH) Représentation des fonctions récursives.

• Séance 6 : 28 février (PH) Lambda-calcul typé : préservation de type et forte normalisation.

• Séance 7 : 6 mars (PH) Fonctions représentables en lambda-calcul typé.

• Séance 8 : 13 mars (KN et/ou PH) Contrôle.

• Séance 9 : 20 mars (KN) Lambda-mu-calcul : Church-Rosser et préservation de type.

• Séance 10 : 27 mars (KN) Plusieurs preuves de forte normalisation du lambda-mu-calcul typé.

• Séance 11 : 3 avril (KN) Entiers classiques et mise en mémoire.

• Séance 12 : 10 avril (PH) Sémantique du lambda-calcul (1).

• Séance 13 : 17 avril (PH) Sémantique du lambda-calcul (2).

• Séance 14 : 24 avril (KN et/ ou PH) Examen final.

Contenu des séances

Séance 1

-- à compléter au fur et à mesure --

Quelques références

• logique générale : "Introduction à la Logique Théorie de la démonstration" de René David, Karim Nour et Christophe Raffalli ; édité par Dunod. (Voir ici pour plus de détails...)

• lambda-calcul : "Lambda-calcul, types et modèles" de Jean-Louis Krivine ; édité par Masson (1990). Cet ouvrage est epuisé, mais il y en a deux exemplaires à la bibliothèque de mathématiques. JL Krivine a également mis la version anglaise de son livre sur sa page web

---

---

Contenu algorithmique des démonstrations mathématiques

Introduction

-- à compléter --

Déduction naturelle et traduction de Gödel

blabla

...