03/03/2005
Jean-Baptiste Joinet (PPS, Université Paris 1)
Réseaux multiplicatifs et distributivité faible

La correction (mais non le type) des réseaux multiplicatifs est conservée par l'inversion d'un lien « par » surmontant un lien « tenseur ». Ce remplacement chirurgical correspond à l'action (par élimination des coupures) du morphisme de distributivité faible i.e. la preuve canonique en MLL de A ou (B et C) |- (A ou B) et C. Dans cet exposé, je donnerai une preuve directe de la complétude de la distributivité faible (obtention des réseaux à partir de tels remplacements à partir d'un ensemble de réseaux générateurs) et ferai le lien avec les « systèmes d'inférence profonde » (Deep inference systems), présentés à PPS l'an dernier par Lutz Strassburger.