Réseau de preuves

Les réseaux de preuves, inventés par le logicien Jean-Yves Girard en 1986 dans le cadre de la logique linéaire, sont 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. 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 et . On définit les réseaux de preuves par induction : Le lien axiome n'a aucune prémisse et a deux conclusions et Le lien coupure a deux prémisses et et aucune conclusion Le lien fois a deux prémisses et et une conclusion Le lien par a deux prémisses et et une conclusion On obtient bien un hypergraphe, où 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éseau 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 est prouvable en logique linéaire multiplicative si et seulement si il existe un réseau correct dont les hypothèses sont et les conclusions sont . 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 sûr) 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 est équivalent à un ensemble d'énoncé qui serait deux à deux conséquence d'un lien axiome.