Description

Cette école thématique s'adresse principalement aux étudiants de master ayant une formation en philosophie, informatique ou mathématiques. Elle est également ouverte aux doctorants et aux chercheurs qui souhaiteraient découvrir la logique linéaire.

Le but est de donner une introduction structurée aux notions et résultats prinxipaux de la logique linéaire. Les seuls pré-requis seront une connaissance des bases de la logique classique et des systèmes formels de démonstration (calcul des séquents et déduction naturelle). L'objectif est de permettre aux participants de comprendre, en particulier, les motivations et origines de la logique linéaire, ses connecteurs logiques, son calcul de séquents, ses réseaux de démonstration, ses sémantiques, les liens avec les logiques classique et intuitionniste, etc. Les cours seront donnés en anglais.

Le programme de l'école est conçu de manière à permettre de suivre les colloques organisés les jours suivants.

Orateurs et documents

• Jean-Baptiste Joinet
  • Introduction
• Olivier Laurent
  • Logique Linéaire Multiplicative
  • Exercices
• Damiano Mazza
  • L'attaque des exponentiels
  • Exercices
• Lionel Vaux
  • Sémantique dénotationnelle de la logique linéaire
  • Exercices

Localisation

L'école aura lieu dans l'amphi Huvelin de l'Université Lyon 3.

Programme

Prérequis

Concernant les bases de calcul des séquents, un tutoriel interactif est disponible en ligne.

Plan

• Introduction
• Le fragment multiplicatif de la logique linéaire
  
  • réseaux de preuve
  • calcul des séquents
  • la coupure
  • modèle relationnel
• Les connecteurs exponentiels
  
  • réseaux de preuve avec boîtes
  • calcul des séquents
  • lien avec la logique intuitionniste
  • complexité implicite
• Sémantique dénotationnelle
  
  • modèle relationnel
  • modèle cohérent
  • orthogonalité