De la logique lineaire a la logique differentielle sans promotion

Giulio Guerrieri

Description

De la logique lineaire a la logique differentielle (sans promotion !) Giulio Guerrieri Universite Paris 7 / Universita Roma Tre 11 mars 2010 Projet Verite & Preuve Giulio Guerrieri (Roma Tre / Paris 7) De la logique lineaire a la logique differentielle (sans promotion !) 11 mars 2010 1 / 27

• modele relationnel de ll


• systeme logique


• logique lineaire


• propositionnelle intuitionniste minimale


• calcul des sequents classique


• correspondance de curry-howard


• logique ?-calcul


• systemes logiques

Sujets

• Logique linéaire
• Correspondance de Curry-Howard
• maths
• cours
• cours de

Informations

• Publié par: profil-urra-2012
• Publié le: 01 mars 2010
• Nombre de lectures: 34
• Langue: Français

Extrait

Grrieri(RiulioGuesiraeD)7TamoP/erinelai´elolaqugideffiiguqalolera`sanslle(ntie´ereram11p

Giulio Guerrieri

11 mars 2010 ProjetP&ervueVretie ´

Delalogiquelin´eaire`alalogiquediff´erentielle (sans promotion !)

Universite´Paris7/Universit`aRomaTre

7/20101s2

11ma102/rs20

Giulio Guerrieri

Universite´Paris7/Universita`RomaTre

11 mars 2010 ProjetVet ´ ri&erPueev

72

Delalogiquelin´eaire`alalogiquediffe´rentielle (sans promotion !)

RomaTre/errieri(iGluoiuGalale`irean´liueqigolaleD)7siraPsp(sanelleneit´ffreeuidgoqi

iraP/erTamoR(ireliueiqogalel)Ds7erriioGuGiulnas(ps3/10

Outline

27ma1120rslalagoqi´naeri`eentielleuediff´er

3

Lemod`elerelationneldeLL

2

Lalogiqueline´aire

1

Introduction

Lalogiqueline´airediff´erentielle

4

3

Lemode`lerelationneldeLL

eairlin´iquealogD)leir7s/eaPamrTRoi(errierGuiouliG

Outline

Lalogiqueline´airediffe´rentielle

4

1

Introduction

2

Lalogiquelin´eaire

20104/2711amsr(slespanenereltieuqi´ffidla`egola

nfniioittuIn elumrof euqitamro edcsitnoer!suoupeducβ-r´!caltione´xe,lucnoituc t!py!eytepedodnn´e,sp´ecification uerpλ!evret-p!emgrromeam li´enami 11rsma

λ-calcul

Notre background : la correspondance de Curry-Howard

Cette correspondance est valable, par exemple, si on prend : commesyst`emelogique:lad´eductionnaturellepropositionnelleintuitionniste minimale commesyste`medecalcul:leλimlsempltten´eypc-ucla Ellepeuteˆtre´etendue`adessyst`emeslogiquesetdecalculplusgrands(second ordre,calculdess´equentsclassique,etc.).

Logique

010272/5iquediff´e`alalogels(napsreneitleel)Ds7riPae/Trmariae´nileuqigolaGi(ioRirreuGreluoi