Public: Tronc-commun Volume: 14H | CourseForm | |
|---|---|
| Titre: | Logique et Informatique |
| Sigle: | LOFO |
| Enseignant: | Akim Demaille |
| Période: | T4 |
| Public: | Tronc-commun |
| Contrôle: | Partiel |
| Durée: | 14H |
| Cours Optionnel: | oui |
| Module: | |
| Prérequis: | |
| Objectifs: | L'objectif n'est pas la logique en soi, mais plutôt de montrer pourquoi les informaticiens, et spécialement les théoriciens de l'informatique, se sont réapproprié la logique ces dernières décennies. Il s'agira de montrer une connexion profonde et assez inattendue entre le calcul d'une part, et la preuve d'autre part. Pour ce faire les 7 séances couvriront différents aspects plus ou moins liés à la logique formelle : 1 Lambda calcul 2 Lambda calcul simplement typé 3 Déduction naturelle en logique classique 4 Calcul des séquents, élimination des coupures 5 TD Lambda Calcul / Systèmes de déduction 6 Logique Intuitionniste 7 Isomorphisme de Curry-Howard Ce cours n'est pas à propos de : * la théorie des modèles * l'algèbre de Boole * les logiques modales * la preuve automatique * les logiques exotiques |
| Documentation: | http://www.lrde.epita.fr/~akim/lofo/ |
| Journal: | |