Difference between revisions of "Courses/LOFO"

From LRDE

 
(5 intermediate revisions by 2 users not shown)
Line 2: Line 2:
 
|title=Logique formelle
 
|title=Logique formelle
 
|acronym=LOFO
 
|acronym=LOFO
|teacher=Akim
+
|teacher=Max
 
|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=Programme Classes Préparatoires
+
|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 calcul
 
|content=1) Lambda calcul
Line 29: Line 31:
 
* les logiques modales
 
* les logiques modales
 
* la preuve automatique
 
* la preuve automatique
* les logiques exotiques"
+
* les logiques "exotiques"
|references=http://www.lrde.epita.fr/~akim/lofo
+
|slides=https://www.lrde.epita.fr/~akim/lofo/handouts/
 
}}
 
}}

Latest revision as of 09:33, 21 March 2017

Titre

Logique formelle

Sigle

LOFO

Enseignant

Maximilien Colange

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 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"
Documentation
Support
Journaux