Difference between revisions of "Courses/LOFO"
From LRDE
(Created page with "{{Course |title=Logique formelle |acronym=LOFO |teacher=Akim |period=S4, Ing1 |audience=Tronc-commun |optional course=oui |module=Sciences Générales |prerequisites=Programme...") |
|||
(17 intermediate revisions by 6 users not shown) | |||
Line 1: | Line 1: | ||
{{Course |
{{Course |
||
+ | |visible=Yes |
||
|title=Logique formelle |
|title=Logique formelle |
||
|acronym=LOFO |
|acronym=LOFO |
||
− | |teacher= |
+ | |teacher=Adrien |
|period=S4, Ing1 |
|period=S4, Ing1 |
||
|audience=Tronc-commun |
|audience=Tronc-commun |
||
+ | |exam type=Partiel |
||
+ | |duration=12h |
||
|optional course=oui |
|optional course=oui |
||
|module=Sciences Générales |
|module=Sciences Générales |
||
+ | |prerequisites=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. |
||
− | |prerequisites=Programme Classes Préparatoires |
||
+ | |objectives=Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique : |
||
− | |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. |
||
+ | * Les systèmes de preuves, qui introduisent la notion de vérité comme construction obtenue à partir d'une série de déductions ; des logiciels de preuve comme COQ ou des langages certifiés comme l'Atelier B en dépendent. |
||
− | |content=1) Lambda calcul |
||
+ | * Le lambda calcul, formalisme de programmation différent des machines de Turing mais tout aussi puissant, que l'on peut typer et qui sert de base à la programmation fonctionnelle. |
||
− | |||
+ | 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 : |
||
− | |||
+ | * Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert. |
||
− | 3) Déduction naturelle pour la logique classique |
||
+ | * Déduction naturelle, logique du premier ordre, normalisation. |
||
− | |||
+ | * Lambda calcul, propriétés et applications. |
||
− | 4) Calcul des séquents, élimination des coupures |
||
⚫ | |||
− | |||
+ | |slides=https://www.lrde.epita.fr/~adrien/notes_logi-lofo_19_20.pdf |
||
− | 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" |
||
− | |references=http://epita.lrde.epita.fr/LOFO-Course |
||
− | http://www.lrde.epita.fr/~akim/lofo |
||
}} |
}} |
Latest revision as of 13:28, 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 :
|
Documentation | |
Support | |
Journaux |