Difference between revisions of "Courses/LOFO"
From LRDE
Line 16: | Line 16: | ||
Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique. |
Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique. |
||
|content=Ce cours est découpé en quatre séances : |
|content=Ce cours est découpé en quatre séances : |
||
− | + | 1) Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert. |
|
− | + | 2) Déduction naturelle, logique du premier ordre, normalisation. |
|
− | + | 3) Lambda calcul, propriétés et applications. |
|
− | + | 4) Lambda calcul simplement typé, isomorphisme de Curry-Howard. |
|
− | |slides=https://www.lrde.epita.fr/~ |
+ | |slides=https://www.lrde.epita.fr/~adrien/notes_logi-lofo_19_20.pdf |
}} |
}} |
Revision as of 14:27, 3 July 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 |
Capacité à comprendre et écrire des preuves par récurrence. Capacité à lire des formules mathématiques et à exprimer des propriétés sous forme de formule. Il est souhaitable mais pas obligatoire d'avoir suivi LOGI. |
Objectifs |
Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique :
Ces deux notions sont reliées par l'isomorphisme de Curry-Howard. Un programme est donc d'une certaine manière une forme de preuve mathématique. |
Plan |
Ce cours est découpé en quatre séances : 1) Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert. 2) Déduction naturelle, logique du premier ordre, normalisation. 3) Lambda calcul, propriétés et applications. 4) Lambda calcul simplement typé, isomorphisme de Curry-Howard. |
Documentation | |
Support | |
Journaux |