Difference between revisions of "Courses/LOFO"

From LRDE

Line 10: Line 10:
 
|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, LOGI
 
  +
|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.
  +
* Le lambda calcul, formalisme de programmation différent des machines de Turing mais tout aussi puissant, 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=# Lambda calcul
 
|content=# Lambda calcul
 
# Lambda calcul simplement typé
 
# Lambda calcul simplement typé

Revision as of 13:18, 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, 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
  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