Difference between revisions of "Courses/LOFO"

From LRDE

 
(16 intermediate revisions by 5 users not shown)
Line 1: Line 1:
 
{{Course
 
{{Course
  +
|visible=Yes
 
|title=Logique formelle
 
|title=Logique formelle
 
|acronym=LOFO
 
|acronym=LOFO
|teacher=Akim
+
|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.
2) Lambda calcul simplement typé
 
  +
|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
 
  +
* Lambda calcul simplement typé, isomorphisme de Curry-Howard.
 
  +
|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://www.lrde.epita.fr/~akim/lofo
 
 
}}
 
}}

Latest revision as of 14:28, 3 July 2020

Titre

Logique formelle

Sigle

LOFO

Enseignant

Adrien Pommellet

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 :

  • 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.
  • 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.

Plan

Ce cours est découpé en quatre séances :

  • Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert.
  • Déduction naturelle, logique du premier ordre, normalisation.
  • Lambda calcul, propriétés et applications.
  • Lambda calcul simplement typé, isomorphisme de Curry-Howard.
Documentation
Support
Journaux