Editing Noncommutative logic (section)

'''Noncommutative logic''' is an extension of [[linear logic]] that combines the [[commutative]] [[logical connective|connective]]s of linear logic with the noncommutative multiplicative [[connective (logic)|connective]]s of the [[Lambek calculus]]. Its [[sequent calculus]] relies on the structure of order varieties (a family of [[cyclic order]]s that may be viewed as a [[combinatorial species|species of structure]]), and the correctness criterion for its [[proof net]]s is given in terms of [[partial permutation]]s. It also has a [[denotational semantics]] in which [[formula (logic)|formula]]s are interpreted by [[module (algebra)|module]]s over some specific [[Hopf algebra]]s.