Marc Bagnol, Le critère de correction Mogbil-Naurois

Programme

Résumé

V. Mogbil et P. Naurois ont établi que la correction des réseaux de preuves M(E)LL est NL-complète en introduisant un nouveau critère de correction, équivalent au critère de Danos-Regnier. J.-Y. Girard a repris l'idée de ce critère dans son dernier article (GdI6) sous le nom de « switchings virtuels », utilisés dans le critère de correction des modalités exponentielles.

Je vous parlerai du critère Mogbil-Naurois: définition, exemples, complexité... et (exclusif!) je donnerai une preuve directe et très simple de séquentialisation des réseaux MLL pour ce critère, sans passer par l'équivalence avec Danos-Regnier.