Editing Noncommutative logic (section)

===BV and NEL===

[[Alessio Guglielmi]] proposed a variation of Retoré's calculus, BV, in which the two noncommutative operations are collapsed onto a single, self-dual, operator, and proposed a novel proof calculus, the [[calculus of structures]] to accommodate the calculus.  The principal novelty of the calculus of structures was its pervasive use of [[deep inference]], which it was argued is necessary for calculi combining commutative and noncommutative operators; this explanation concurs with the difficulty of designing sequent systems for pomset logic that have cut-elimination.

Lutz Straßburger devised a related system, NEL, also in the calculus of structures in which linear logic with the mix rule appears as a subsystem.