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=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.
 
|objectives=Ce cours présente principalement deux notions théoriques avec des applications concrètes en informatique :
 
|objectives=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.
 
* 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.
+
* 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.
 
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=Ce cours est découpé en quatre séances :
  +
1) Logique propositionnelle et sa sémantique, preuves, systèmes à la Hilbert.
# Lambda calcul simplement typé
 
# Déduction naturelle pour la logique classique
+
2) Déduction naturelle, logique du premier ordre, normalisation.
  +
3) Lambda calcul, propriétés et applications.
# Calcul des séquents, élimination des coupures
 
# TD Lambda Calcul / Systèmes de déduction
+
4) Lambda calcul simplement typé, isomorphisme de Curry-Howard.
# Logique Intuitionniste
 
# 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"
 
 
|slides=https://www.lrde.epita.fr/~akim/lofo/handouts/
 
|slides=https://www.lrde.epita.fr/~akim/lofo/handouts/
 
}}
 
}}

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