Noncommutative Logic

Noncommutative logic is an extension of linear logic which combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek calculus (see External links below). Its sequent calculus relies on the structure of order varieties (a family of cyclic orders which may be viewed as a species of structure), and the correctness criterion for its proof nets is given in terms of partial permutations. It also has a denotational semantics in which formulas are interpreted by modules over some specific Hopf algebras.