Sujet de programmation pour un master en informatique
Christian Retoré ( retore@labri.fr / 05 40 00 38 72 )
Les réseaux de démonstration sont des graphes qui représentent fidèlement les preuves de la logique linéaire.[1] Ces graphes admettent une définition inductive fournie par les règles de la logique, mais aussi une caractérisation purement combinatoire. Un réseau de démonstration est un graphe muni d'un couplage parfait, dont les autres arêtes constituent un cographe, et qui satisfait le critère suivant: tout cycle élémentaire alternant les arêtes du couplage et celles du cographe contient une corde (une arête joignant deux sommets du cylce mais ne faisant pas partie du cycle).
Une variante de la logique linéaire appelée Pomset Logic définit un réseau de démonstration exactement de la même manière, à ceci près que le cographe est un cographe orienté, c'est-à-dire qu'il appartient à la plus petite classe de graphe contenant les graphes à un sommet (sans arête), close par somme disjointe, par composition en série et par composition en série orientée (toutes les arêtes sont alors orientées d'une partie vers l'autre.[2] Le critère de correction reste le même en version orientée:
Dans ce cas, en dépit des propriétés logiques de ces graphes (élimination des coupres, sémantique dénotationnelle fidèle dans le cadre des espaces cohérents) il n'a pas été possible de donner un calcul des séquents pour ce calcul ou une définition inductuve de ces graphes. Il faudrait pour cela établie la conjecture suivante: dans un réseaux de démonstration orienté, il existe toujours une partition des sommets du graphe en deux classes A et B de sorte qu'il n'y ait aucune arête du couplage entre A et B et que les seules arêtes entre A et B satisfassent l'une des propritété suivantes :
Ce sujet de programmation consistera tout d'abord en la définition d'une structure de données adaptée à la représentation et à la manipulation de ces graphes bicolores, qui permette par exemple de passer d'une présentation matricielle à celle en termes issue des cographes. On prévoira aussi que le cographe peut souhaiter distinguer certaines composition en série, ce qui revient à avoir d'autres couleurs pour les arêtes, et qu'on peut souhaiter tester des propriétés similaires, avec éventuellement des arêtes supplémentaire n'appartenant pas au cographe.
Frédéric Gilbert et Marc AntoineTurbet-Delof ont déjà écrit un programme qui permet de visualiser ces graphes avec Tulip et qui vérifie si tout circuit élémentaire alternant contient une corde. [5]
Les modules suivants sont à réaliser :
Tout langage de programmation est possible mais ce sera plsu facile en C++ en raison de l'interface avec Tulip.
[0] Un exposé récent sur ces questions: Graphes de démonstrations, cographes et couplages parfaits.
[1] Girard, J.-Y. : Linear Logic, Theoretical Computer Science, 50:1, pp. 1-102, 1987.
[2] Christian Retoré Handsome proof nets: perfect matchings and cographs. Theoretical Computer Science. 294(3), 2003, pages 473–488 Voi aussi: http://hal.inria.fr/docs/00/07/30/20/PDF/RR-3652.pdf
[3] Christian Retoré Pomset logic as a calculus of directed cographs In V.~M.~Abrusci and C.~Casadio (Eds) Dynamic Perspectives in Logic and Linguistics: Proof Theoretical Dimensions of Communication Processes,Proceedings of the 4th Roma Workshop , Edizione Bulzoni, Roma, 1999 ISBN 8319-443-8. pp 221 -- 247 https://hal.ccsd.cnrs.fr/docs/00/07/29/53/PDF/RR-3714.pdf
[4] Frédéric Gilbert et Marc-Antoien Turbet-Delof Graphes de démosntration en logique linéaire. Programme et compte rendu. Master Informatique, Université Bordeaux Avril 2008.