PUBLICATIONS DE L'INSTITUT MATHEMATIQUE (BEOGRAD) (N.S.) Vol. 78(92), pp. 1–33 (2005) 

COHERENCE OF ProofNet CATEGORIESKosta Dosen and Zoran PetricMatematicki institut SANU, Beograd, Serbia and MontenegroAbstract: The notion of proofnet category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proofnet categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proofnet category catches the unit free fragment of the notion of starautonomous category, a special kind of symmetric monoidal closed category. Keywords: generality of proofs; linear logic; mix; proof nets; linear distribution; dissociativity; categorial coherence; KellyMac Lane graphs; Brauerian graphs; split equivalences; symmetric monoidal closed category; starautonomous category Classification (MSC2000): 03F07; 03F52; 18D10; 18D15; 19D23 Full text of the article: (for faster download, first choose a mirror)
Electronic fulltext finalized on: 2 Mar 2006. This page was last modified: 27 Oct 2006.
© 2006 Mathematical Institute of the Serbian Academy of Science and Arts
