Thirty years ago, I introduced a non-commutative variant of classical linear logic, called "pomset logic", issued from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a non-commutative connective, "$\triangleleft$" called "before", associative and self-dual: $(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$. The conclusion of a pomset logic proof is a Partially Ordered MultiSET of formulas. Pomset logic enjoys a proof net calculus with cut-elimination, denotational semantics, and faithfully embeds sequent calculus. The study of pomset logic has reopened with recent results on handsome proof nets, on its sequent calculus, or on its following calculi like deep inference by Guglielmi and Strassburger. Therefore, it is high time we published a thorough presentation of pomset logic, including published and unpublished material, old and new results. Pomset logic (1993) is a non-commutative variant of linear logic (1987) as for Lambek calculus (1958!) and it can also be used as a grammatical formalism. Those two calculi are quite different, but we hope that the algebraic presentation we give here, with formulas as algebraic terms and with a semantic notion of proof (net) correctness, better matches Lambek's view of what a logic should be.

翻译：三十年前，我基于线性逻辑在相干空间这一特定范畴论解释下的成果，提出了一种经典线性逻辑的非交换变体，称为“pomset逻辑”。除了线性逻辑中常见的交换乘法连接词外，pomset逻辑还包含一个名为“before”、记作“$\triangleleft$”的非交换连接词，它兼具结合性与自对偶性：$(A\triangleleft B)^\perp=A^\perp \triangleleft B^\perp$。pomset逻辑证明的结论是一个公式的偏序多重集（Partially Ordered MultiSET）。pomset逻辑具备带有切割消去的证明网演算、指称语义，并能忠实嵌入相继式演算。近年来，由于在优美证明网、相继式演算以及Guglielmi和Strassburger提出的深度推理等后继演算方面取得新成果，pomset逻辑的研究重新活跃起来。因此，现在正是时候发表一份关于pomset逻辑的全面阐述，内容涵盖已发表与未发表的资料、新旧研究成果。pomset逻辑（1993年）作为线性逻辑（1987年）的非交换变体，其地位类似于Lambek演算（1958年！），同时也可用作语法形式体系。这两种演算差异显著，但我们希望本文以公式作为代数项、并采用语义性证明（网）正确性概念的代数化阐述，能更贴合Lambek对逻辑应有形态的见解。