Difference between revisions of "Courses/LOFO"
From LRDE
Line 1: | Line 1: | ||
{{Course |
{{Course |
||
+ | |visible=No |
||
|title=Logique formelle |
|title=Logique formelle |
||
|acronym=LOFO |
|acronym=LOFO |
||
Line 11: | Line 12: | ||
|prerequisites=Programme Classes Préparatoires, LOGI |
|prerequisites=Programme Classes Préparatoires, LOGI |
||
|objectives=Le véritable but de ce cours est de présenter l’isomorphisme de Curry-Howard, qui montre une correspondance profonde, et surprenante, entre le programmes et démonstrations. À cette fin tous les prérequis sont introduits dans un premier temps. Ils sont intéressants en soi pour la culture de l’informaticien sensible aux aspects formels. |
|objectives=Le véritable but de ce cours est de présenter l’isomorphisme de Curry-Howard, qui montre une correspondance profonde, et surprenante, entre le programmes et démonstrations. À cette fin tous les prérequis sont introduits dans un premier temps. Ils sont intéressants en soi pour la culture de l’informaticien sensible aux aspects formels. |
||
+ | |content=1) Lambda calcul2) Lambda calcul simplement typé3) Déduction naturelle pour la logique classique4) Calcul des séquents, élimination des coupures5) TD Lambda Calcul / Systèmes de déduction6) Logique Intuitionniste7) Isomorphisme de Curry-HowardCe 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" |
||
− | |content=1) Lambda calcul |
||
− | |||
− | 2) Lambda calcul simplement typé |
||
− | |||
− | 3) Déduction naturelle pour la 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" |
||
|slides=https://www.lrde.epita.fr/~akim/lofo/handouts/ |
|slides=https://www.lrde.epita.fr/~akim/lofo/handouts/ |
||
}} |
}} |
Revision as of 15:10, 3 February 2020
Titre |
Logique formelle |
---|---|
Sigle |
LOFO |
Enseignant | |
Période |
S4, Ing1 |
Public |
Tronc-commun |
Contrôle |
Partiel |
Durée |
12h |
Optionnel |
oui |
Module |
Sciences Générales |
Prérequis |
Programme Classes Préparatoires, LOGI |
Objectifs |
Le véritable but de ce cours est de présenter l’isomorphisme de Curry-Howard, qui montre une correspondance profonde, et surprenante, entre le programmes et démonstrations. À cette fin tous les prérequis sont introduits dans un premier temps. Ils sont intéressants en soi pour la culture de l’informaticien sensible aux aspects formels. |
Plan |
1) Lambda calcul2) Lambda calcul simplement typé3) Déduction naturelle pour la logique classique4) Calcul des séquents, élimination des coupures5) TD Lambda Calcul / Systèmes de déduction6) Logique Intuitionniste7) Isomorphisme de Curry-HowardCe 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 | |
Support | |
Journaux |