  This paper introduces a logical system, called BV, which extends
multiplicative linear logic by a non-commutative self-dual logical operator.
This extension is particularly challenging for the sequent calculus, and so far
it is not achieved therein. It becomes very natural in a new formalism, called
the calculus of structures, which is the main contribution of this work.
Structures are formulae submitted to certain equational laws typical of
sequents. The calculus of structures is obtained by generalising the sequent
calculus in such a way that a new top-down symmetry of derivations is observed,
and it employs inference rules that rewrite inside structures at any depth.
These properties, in addition to allow the design of BV, yield a modular proof
of cut elimination.
