Došen, Kosta; Petrić, Zoran Coherence of proof-net categories. (English) Zbl 1274.03089 Publ. Inst. Math., Nouv. Sér. 78(92), 1-33 (2005). Summary: The notion of proof-net 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 and Mac Lane’s coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit-free fragment of the notion of star-autonomous category, a special kind of symmetric monoidal closed category. Cited in 2 Documents MSC: 03F07 Structure of proofs 03F52 Proof-theoretic aspects of linear logic and other substructural logics 18A10 Graphs, diagram schemes, precategories 18A15 Foundations, relations to logic and deductive systems 18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.) Keywords:generality of proofs; linear logic; mix principle; proof nets; linear distribution; dissociativity; categorial coherence; Kelly-Mac Lane graphs; Brauerian graphs; split equivalences; symmetric monoidal closed category; star-autonomous category PDFBibTeX XMLCite \textit{K. Došen} and \textit{Z. Petrić}, Publ. Inst. Math., Nouv. Sér. 78(92), 1--33 (2005; Zbl 1274.03089) Full Text: DOI arXiv EMIS