Comment jouer la logique lineaire? Hirschowitz Introduction Les positions Comment jouer la logique lineaire? Les coups Les parties Les strategies 1Andre HirschowitzLes exponentielles 2MichelwitzConclusions 3Tom Hirschowitz 1 2 3CNRS, UNS CEA - LIST CNRS, Universite de Savoie Paris 1/12/2008Comment jouer la logique lineaire? Le probleme Hirschowitz Introduction Les positions Les coups Les parties Les strategies Trouver une de nition de la verite independante des preuves Les exponentielles via les jeux (de la semantique) en esperant l’eliminationConclusions des coupures et la consistance gratuites ... en logique lineaire en esperant un tiers-exclu gratuit...Comment jouer la logique lineaire? Les niveaux Hirschowitz Introduction Les positions Les coups Les parties Les strategies 1 pour MALL Les exponentielles 2 + exponentiellesConclusions 3 + quanti cateurs du premier ordre 4 + choix? + tiers-exclu?Comment jouer la logique lineaire? Travaux connexes Hirschowitz Introduction Les positions Les coups Modeles de la logique lineaire Les parties Les strategies Abramsky-Jagadeesan-Malacaria, Hyland-Ong, Nickau. Les exponentielles Abramsky-Mellies, Mellies. Conclusions Girard. Delande-Miller. Mellies-Mimram. L’incontournable standard: "Full completeness".Comment jouer la logique lineaire? Les resultats Hirschowitz Introduction Les positions Un jeu graphique (ou topologique, les positions sont des Les coups graphes etiquetes), Les parties avec un coup Cut (et Mix si on veut) ...
Andre´Hirschowitz1 Michel Hirschowitz2 Tom Hirschowitz3
Le probleme `
vialesjeux(delase´mantique)e´rantl’´elimination n espe des coupures et la consistance gratuites ... enlogiquelin´eaireenesp´erantuntiers-exclugratuit...
Un jeugraphique(outopologique, les positions sont des graphes´etiquet´es), avec un coupCut(etMixsi on veut). Lesstrat´egiesgagnantesconstituentunmod`elecorrect etcoh´erent, Avece´liminationdescoupurespourlefragmentMALL. Lescoupssontdesmorphismesdansunecate´gorieG. L’´eliminationdescoupuresde´couled’unsyst`emede factorisation dans G.
mais aujourd’hui Priorite´auxexponentielles
Sans toucher au jeu. Enchangeantlanotiondestrate´gie Pourunenotiondestrate´giepluslocale(innocente?)