Une représentation graphique et canonique des preuves pour des fragments de la logique linéaire où formules et connexions deviennent nœuds et liens ; les réseaux de preuves mettent au jour le parallélisme, éliminent la bureaucratie syntaxique des preuves en sequent et permettent des critères de correction graphiques ainsi qu'une élimination des coupures par transformations locales de graphe.

Principe

Coder une preuve sous la forme d'une structure en graphe (liens pour les connecteurs logiques et liens d'axiome pour paires atomiques) de sorte que des conditions de correction permettent d'identifier les graphes correspondant à des preuves séquent valides ; l'élimination des coupures se réalise par réécritures locales du graphe préservant la correction.

Démonstration

En logique linéaire multiplicative, une dérivation de A⊗B se représente par un réseau comportant un lien tensor réunissant les sous-réseaux pour A et B et des liens d'axiome appariant les atomes duaux ; une condition de correction (acyclicité et connexité sous des 'switchings') certifie que le diagramme est une preuve valide et que les réécritures de graphe réalisent l'élimination des coupures.

Mauvaise application

Considérer comme réseau de preuves tout graphe arbitraire aux degrés similaires sans vérifier les conditions de correction prescrites, ou appliquer des transformations de réseaux issues d'un fragment incompatibles avec un autre, peut produire des « preuves » non valides ou briser les invariants d'élimination des coupures.

Conséquence

Correctement formés, les réseaux de preuves offrent un témoin canonique et souvent compact de la provabilité, rendent le parallélisme explicite, simplifient l'équivalence des preuves et transforment l'élimination des coupures en réécritures locales et confluentes du graphe—ce qui facilite les analyses de complexité et de normalisation.

Inversion

La vue opposée est la preuve séquentielle : une dérivation linéarisée, règle par règle, qui enregistre explicitement l'ordre d'application des règles. Les preuves séquentiales rendent le comportement opérationnel visible mais masquent la structure parallèle et présentent de nombreuses variantes syntaxiques d'un même réseau.

Limite

Les réseaux de preuves sont mûrement développés pour plusieurs fragments de la logique linéaire (multiplicatif, multiplicatif-exponentiel avec précautions) mais exigent des schémas de liaison et des critères de correction adaptés à chaque fragment ; ils ne constituent pas une représentation graphique immédiatement applicable à des logiques non linéaires ou classiques sans adaptation.

Tension sémantique

Tension entre réseaux de preuves et présentations en sequent : les réseaux privilégient une structure canonique et parallèle des preuves tandis que les séquents affichent l'ordre syntaxique des dérivations ; la conversion réciproque (séquentialisation) est souvent subtile et dépend du fragment considéré.

Synthèse

Les réseaux de preuves condensent les dérivations séquentielles en objets graphiques qui rendent explicite la structure parallèle essentielle des preuves en logique linéaire : en imposant des vérifications de correction précises et en traitant l'élimination des coupures comme réécritures de graphe, ils fournissent un compte rendu compact et transparent des preuves et de leur normalisation.