Réseaux de preuves

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Les réseaux de preuves, inventés par le logicien Jean-Yves Girard en 1986 dans le cadre de la logique linéaire, est un outil de démonstration formel pour cette même logique (c'est-à-dire une alternative aux séquents qui sont aussi employés en logique classique et intuitionniste). Grossièrement, il s'agit d'un équivalent de la déduction naturelle de la logique intuitionniste adaptée à la logique linéaire. Ils s'en différencient cependant par le caractère géométrique de cette approche : une preuve est formée par un hypergraphe et le critère de correction peut s'exprimer comme un parcours de graphe.

Définition[modifier | modifier le code]

Définition inductive des réseaux de preuves pour MLL[modifier | modifier le code]

Les réseaux de preuves peuvent être définis pour différents fragments de la logique linéaire, on se restreint dans un premier temps au fragment multiplicatif (MLL) c'est-à-dire uniquement avec les symboles \otimes et \wp .

On définit les réseaux de preuves par induction :

  • Le lien axiome n'a aucune prémisse et a deux conclusions A et A^\bot
  • Le lien coupure a deux prémisses A et A^\bot et aucune conclusion
  • Le lien fois a deux prémisses A et B et une conclusion A \otimes B
  • Le lien par a deux prémisses A et B et une conclusion A \wp B

On obtient bien un hypergraphe, ou les liens sont orientés de ses prémisses vers ses conclusions. On remarque :

  • tout énoncé est prémisse d'au plus un lien
  • tout énoncé est conclusion d'au plus un lien

On appelle alors :

  • hypothèse du réseaux un énoncé qui n'est conclusion d'aucun lien
  • et conclusion du réseau un énoncé qui n'est prémisse d'aucun lien

Le critère de correction énonce alors que le séquent A_1, \ldots, A_n \vdash B_1, \ldots, B_m est prouvable en logique linéaire multiplicative si et seulement si il existe un réseau correct dont les hypothèses sont A_1, \ldots, A_n et les conclusions sont  B_1, \ldots, B_m .

Réseaux à boîtes[modifier | modifier le code]

La logique linéaire restreinte au fragment multiplicatif est relativement peu expressive. Une extension des réseaux de preuves à MELL, c'est-à-dire aux exponentielles ! (bien sur) et ? (pourquoi pas), est possible mais nécessite l'ajout de la notion de boîte. Une boîte est la généralisation d'un lien axiome : vu de l'extérieur, une de boîte conclusion A_1, \ldots, A_n est équivalent à un ensemble d'énoncé A_1, \ldots, A_n qui serait deux à deux conséquence d'un lien axiome. À l'intérieur de la boîte on place un séquent quelconque qui a été prouvé de manière externe. On peut donc voir les boîtes comme un moyen d'intégrer aux réseaux de preuves des éléments provenant de l'extérieur, c'est-à-dire du calcul des séquents.

Pour intégrer les exponentielles à notre calcul, on se place dans le cadre du calcul mixte, c'est-à-dire que l'on se donne la possibilité de souligner n'importe quelle conclusion de lien, dénotant ainsi une gestion classique et non plus linaire de l'énoncé :

  • L'introduction de bien sur se fait en plaçant un réseaux de conclusion  A_1, \ldots, A_n, B dans une boîte de conclusion \underline{A_1}, \ldots, \underline{A_n}, !B
  • L'introduction de pourquoi pas se fait en plaçant un lien ayant pour prémisses n occurrences de \underline{A} et pour conclusion  ? A

On remarque que :

  1. Dans les deux cas, n est éventuellement nul.
  2. Dans le cas du bien sur on peut supposer que le réseaux n'a que des conclusions et pas de prémisses quitte à rajouter des liens axiomes (un prémisse  A devient une conclusion  A^\bot )
  3. Le lien pourquoi pas correspond à l'affaiblissement dans le cas 0-aire, à la déréliction dans le cas unaire et à la contraction dans le cas n-aire pour  n \geq 1

Les quantificateurs[modifier | modifier le code]

L'ajout de quantificateurs au premier ordre est assez immédiat, on ajoute deux liens :

  • Le lien pour tout a pour prémisse un énoncé  A et pour conclusion  \forall x A x est une variable fraiche ou eigenvariable
  • Le lien il existe a pour prémisse un énoncé  A[t/x] et pour conclusion  \exist x A . La notation A[t/x] dénote alors la substitution de la variable x par le terme t dans l'énoncé A.

Les additifs[modifier | modifier le code]

L'ajout des additifs aux réseaux de preuves constitue une tâche difficile si l'on tente de le faire en l'absence de boîtes. Les divers critères de correction proposés pour les réseaux additifs sans boîtes ne font pas l'unanimité chez les spécialiste du domaine.

Critères de correction[modifier | modifier le code]

Un critère de correction est un critère permettant de caractériser les réseaux correspondant à des preuves dans le calcul des séquents. En effet, alors que les séquents ont une correction locale (suivi des régles du calcul considéré) et une élimination des coupures globales, les réseaux de preuves ont une correction globale et une élimination des coupures locales.

Critère original[modifier | modifier le code]

Le critère original dû à Jean-Yves Girard s'exprime en termes de voyage dans un réseau : on simule le trajet d'une particule le long des hyperarrêtes du réseau.

Critère de Danos-Regnier[modifier | modifier le code]

On introduit la notion d'interrupteur : un interrupteur I sur un réseau de preuve est un choix d'orientation de chaque lien par de ce réseau, c'est-à-dire on considère que chaque lien par n'est relié qu'à une seule de ses deux prémisses. Si un réseau contient n liens par, il y a alors 2^n interrupteurs.

Le critère s’énonce alors ainsi : Un réseau de preuve est correct si et seulement si il est connexe et acyclique pour tout choix d'interrupteur, c'est-à-dire si et seulement si pour tout choix d'interrupteur le graphe obtenu est un arbre.

Critère pour les réseaux avec boites[modifier | modifier le code]

Le critère précédent s'étend facilement au cas des boîtes : Un réseau à boîte est correct si les réseaux contenus dans chaque boîte sont corrects et si le réseau obtenu en remplaçant chaque boîte par une hyperarrête l'est aussi (au sens précédent).

Le traitement des exponentielles se fait alors de la manière suivante :

  • L'introduction de bien sur se fait avec la méthode ci-dessus.
  • Le lien pourquoi pas peut être considéré comme une généralisation d'un lien par : on généralise la notion d'interrupteur en demandant à faire un choix d'une prémisse pour chaque lien pourquoi pas.

Critère pour les réseaux à quantificateurs[modifier | modifier le code]