Discussion:Réseau de preuves
- Admissibilité
- Neutralité
- Droit d'auteur
- Article de qualité
- Bon article
- Lumière sur
- À faire
- Archives
- Commons
 Tâches à accomplir pour Réseau de preuves
|
aide | |
| ||
Graphiques[modifier le code]
Il serait très utile d'avoir des graphiques des différents nœuds utilisés pour les réseaux de preuves, des boîtes ainsi éventuellement qu'un exemple de réseau correct avec l'application du critère de correction.
Dans le paragraphe réseaux à boîtes, il me semble qu'il y ait un formalisme plus intuitif des exponentielles en utilisant une boîte pour le nœud ! qui a pour prémisses ?A_1, ... , ?A_n, B conclusion ?A_1, ... , ?A_n, !B, et en utilisant 3 nœuds ?_w pour l'affaiblissement (pas de prémisse et une conclusion de type ?A), ?_d pour la déréliction (une prémisse de type A et une conclusion de type ?A) et ?_c pour la contraction (deux prémisses de types ?A toutes les deux, et une conclusion de type ?A).
Enfin, dans la section critères de correction, ce serait bien d'avoir une preuve du critère de Danos-Regnier par exemple (le plus utilisé), au moins pour le sens facile réseau de preuve correcte ==> critère de correction (la séquentialisation est plus délicate, mais une preuve récente plus simple dûe à Paolo Di Giamberardino et Claudia Faggian permet d'éviter la preuve originelle de Girard avec les empires : http://www.pps.univ-paris-diderot.fr/~faggian/pubs/jump.pdf).
--2001:660:3301:8061:DC60:C374:86B5:58C3 (d) 20 août 2012 à 17:57 (CEST)