Coherence of proof-net categories

DOI10.2298/PIM0578001DMaRDI QIDQ4928272zbMATH OpenFDO

Authors Kosta Došen, Zoran Petrić

Publication date 10 June 2013

Published in Publications de l'Institut Math?matique (Belgrade) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0503301, http://www.emis.de/journals/PIMB/092/1.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

Brauerian graphscategorial coherencedissociativitygenerality of proofsKelly-Mac Lane graphslinear distributionlinear logicmix principleproof netssplit equivalencesstar-autonomous categorysymmetric monoidal closed category

Mathematics Subject Classification ID

Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Graphs, diagram schemes, precategories (18A10) Foundations, relations to logic and deductive systems (18A15) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Abstract: 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's 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.

Recommendations

• Proof-net categories
• scientific article; zbMATH DE number 517045
• Coherence in linear predicate logic
• Natural deduction and coherence for weakly distributive categories
• Linear logic, coherence and dinaturality

Cited in

(26)

• Coherence in linear predicate logic
• Natural deduction and coherence for weakly distributive categories
• Coherent models of proof nets
• Proof of a conjecture of S. Mac Lane
• Coherence completions of categories
• Coherence in substructural categories
• Coherence for star-autonomous categories
• Categorical semantics of linear logic
• Generalised Proof-Nets for Compact Categories with Biproducts
• Cartesian isomorphisms are symmetric monoidal: A justification of linear logic
• scientific article; zbMATH DE number 517045 (Why is no real title available?)
• On cyclic star-autonomous categories
• scientific article; zbMATH DE number 1373514 (Why is no real title available?)
• Obsessional experiments for linear logic proof-nets
• Coherent interaction graphs
• Proof nets, coends and the Yoneda isomorphism
• Coherence for Frobenius pseudomonoids and the geometry of linear proofs
• CATEGORICAL HARMONY AND PATH INDUCTION
• From Proof Nets to the Free *-Autonomous Category
• Proof-net categories
• Proof nets and semi-star-autonomous categories
• Rewriting in Gray categories with applications to coherence
• Linear logic, coherence and dinaturality
• Coherence in Cartesian closed categories and the generality of proofs
• A categorical semantics for polarized MALL
• Equality of proofs for linear equality

This page was built for publication: Coherence of proof-net categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928272)