Accueil
Connexion
DENIF –
Documents d’Enseignement Numériques en Informatique Fondamentale
Thèmes
Cursus
Enseignants
Logique
Thème :
Logique & Preuve
–
Cursus :
ENS-Lyon - L3
2005 - 2006
Cours
Pierre Lescanne
Introduction à la logique
Calcul à la Hilbert
La déduction naturelle
Les séquents
La logique propositionnelle classique
Introduction au lambda-calcul
Introduction au lambda-calcul - généralités
Introduction au lambda-calcul - logique combinatoire
Lambda-calcul simplement typé
Introduction au calcul des prédicats du premier ordre
Complétude du calcul propositionnel intuitionniste
Les modèles de Kripke de la logique propositionnelle intuitionniste
TDs
Il manque les TDs 8 et 9. Plus de la moitié des TDs sont repris de l'année précédente.
Stéphane Le Roux
,
Vincent Nesme
TD 0 Déduction naturelle
TD 1 Introduction à la logique
TD 2 Logique minimale de Hilbert, logique propositionnelle intuitionniste
TD 3 Déduction naturelle
TD 3 bis Déduction naturelle
TD 4 Début du lambda-calcul
TD 5 lambda-calcul
TD 6 récriture et lambda-calcul
TD 7 lambda-calcul, types et logique combinatoire
TD 10 Modèles
TD 11 Théorie des ensembles
TD 12 Modèles de Kripke
Examens
Pierre Lescanne
,
Stéphane Le Roux
,
Vincent Nesme
Partiel
Examen
Corrigé de l'examen
2004 - 2005
TDs
Pas de corrigé pour le TD 4. Insiprés des TDs de Romain Kervarc.
Sylvie Boldo
,
Stéphane Le Roux
TD 1 : introduction à la logique (modèle 0,1 et des arbres de preuves en théorie des groupes)
Corrigé
TD 2 : logique minimale de Hilbert et logique propositionnelle intuitionniste
Corrigé
TD 3 : déduction naturelle
Corrigé
TD 4 : lambda-calcul
TD 5 : encore du lambda-calcul
Corrigé
TD 6 : types simples
Corrigé
TD 7 : lambda-calcul, réduction
Corrigé
TD 8 : logique combinatoire
Corrigé
TD 9 : modèles de Kripke
Corrigé
TD 10 : modèles
Corrigé
TD 11 : théorie des ensembles
Corrigé
TD 12 : logique epistémique
Corrigé
Examens
Sylvie Boldo
,
Pierre Lescanne
,
Stéphane Le Roux
Partiel
Correction du partiel
Examen