21/06/2001: Virgile Mogbil (IML, Marseille)
Un crit�re de correction quadratique pour la logique non commutative.

Résumé
La logique non commutative (NL) d�velopp�e par P.Ruet est une g�n�ralisation de la logique lin�aire (LL) et de la logique cyclique lin�aire (extension conservative du calcul de Lambek). C'est � dire que le calcul des s�quents autorise la cohabitation de connecteurs commutatifs et non commutatifs.
S.Guerrini a montr� que la correction des r�seaux de preuve multiplicatifs de LL se fait en temps lin�aire. On est loin de ce r�sultat en logique non-commutative multiplicative (MNL) : on conna�t un crit�re utilisant les longs voyages � la J.-Y.Girard (M.Abrusci et P.Ruet) et r�cemment R.Maieli en a montr� un � la Danos-Regnier. Ils sont donc en temps exponentiel.
Le travail que je vais pr�senter est une premi�re �tape vers un algorithme en temps lin�aire. On �tablit un crit�re de contraction pour MNL qui pr�sente l'avantage d'�tre en temps quadratique. Il se pr�sente sous la forme de r�gles de r��criture inspir�es par le calcul des s�quents de MNL. On des r�sultats de confluence, d'ad�quation et de s�quentialisation.
Enfin, les pr�c�dents crit�res connus ne fonctionnent pas avec la r�gle de coupure alors que celui-ci peux y �tre �tendu sans en changer la complexit� (on a alors de bonnes propri�t�es comme la pr�servation de la correction par �limination des coupures, acyclicit� et connexit� des r�seaux de preuve de MNL, ...). Il g�n�ralise alors le crit�re de contraction de V.Danos.