Abstract FR:

Nous etudions les reseaux de preuves de la logique lineaire multiplicative, tout d'abord en presence de la regle de melange et des elements neutres, puis pour un calcul ou la conclusion d'une preuve est un multi-ensemble ordonne de formules, ce dernier etant concu comme un modele du parallelisme. Le premier calcul satisfait le theoreme de sequentialisation: tout reseau correct correspond a une preuve du calcul des sequents. C'est la consequence d'un resultat sur la connexite d'une generalisation des graphes ou une arete est un graphe biparti-complet. On donne un calcul en reseaux pour les connecteurs n-aires definis par des ordres, dont le precede, binaire, associatif, non-commutatif et autodual. Le critere de correction est: il n'y a pas de circuit utilisant au plus une arete de chaque lien par ou precede. On sait en calculer la semantique coherente, il existe un calcul en sequents correspondant et les connecteurs definissables au moyen de par et precede sont caracterises par un theoreme sur les ordres finis