Prochain séminaire/GdT :

Réseaux de preuve pour MLL+Mix et algorithmes sur les graphes arêtes-coloriés
guyễn Lê Thành Dũng (future LIPN ?)
Salle B107, bâtiment B, Université de Villetaneuse
16/11/2017 11:00 - 12:30
Résumé :

Le critère de correction de Danos-Regnier mène à poser le problème d'algorithmique des graphes suivant : étant donné un graphe apparié, trouver un cycle (ou un chemin) passant au plus une fois par chaque paire. Ce problème a été traité en théorie des graphes sous la forme plus générale de graphes munis d'une coloration sur leurs arêtes ("edge-colored graphs") ; la solution fait intervenir une réduction aux couplages parfaits et rejoint donc le travail de C. Retoré sur les "handsome proof-nets".

Partant de cela, on obtient facilement d'une part un critère de correction pour MLL+Mix en temps linéaire, et d'autre part que le problème de correction des réseaux MLL+Mix est probablement plus difficile que celui pour MLL sans la règle Mix (qui est NL-complet). Ce dernier résultat explique que la littérature sur les critères de correction pour MLL+Mix soit plus maigre que celle pour MLL. Nous verrons également d'autres conséquences de ces liens entre logique linéaire et théorie des graphes, notamment en lien avec le graphe de dépendances d'un réseau introduit par Bagnol, Doumane et Saurin.

Séminaires/GdT à venir (peut changer)

Séminaires/GdT passés