Duality
-------

The dual of an object will be denoted by a prefixed co: par -> copar,
rule -> corule, derivation -> coderivation, etc.


Notation for contexts
---------------------

[ , , ] is the "par";
( , , ) is the "tensor" or "co-par" or "and";
< ; ; > is the "seq";

S{ } denotes a structure with a hole.

The braces surrounding a context, like in S{[a,b]}, can be dropped
wherever convenient, like in S[a,b].

[ , , ] and ( , , ) may be made additive (say) by the superposition of
little bullets, or circles.


Names of systems
----------------

Principles:

1) The main letter or letters identifying a system stay in the middle;
examples: V, L (for linear logic), K (for classical logic).  The main
letter identifies the core, non-exponential structure of a system: for
example, V stands for 2-dual-comm/1-selfdual-noncomm; W stands for
2-dual-comm/2-dual-noncomm, etc.

2) A known system in the calculus of sequents that is ported to the
calculus of structures gets an S after its name; example: LS is linear
logic in the calculus of structures, KS is classical logic.

3) The "big variant" letters go in front of the main ones; examples:
ELS, EV. The non-exponential, non-additive part of any system is called
"basic" (B).

4) Letters indicating a restriction or "small variant" of a system go in
lowercase after the main ones, in alphabetical order.  Example: core
symmetric basic system V is SBVc.

5) The top-down symmetric variant of a system is denoted by a prefixed
S, and is called the "symmetric" or "self-dual" variant.

6) Common sense is to be applied.

system                   old name   new name
--------------------------------------------

multiplicative system V     MV         BV   (becomes basic system V)
symmetric multiplicative
system V                   SMV        SBV   (becomes self-dual basic system V)
combinatorial system V      CV         BV?  (to be announced)
elementary system V         EV         BV?  (to be announced)
flat multiplicative
system V                   FMV        FBV   (becomes flat basic system V)
multiplicative exponential
system V                   MEV         EV   (becomes exponential system V,
                                             will be dubbed V if it's undecidable)
MELL in the calculus of
structures                             ELS

classical logic                         KS
classical logic in the
self-dual presentation      SC         SKS


Rules
-----

Normally, names of rules will be one-letter, plus arrow.  Super rules or
other variant rules will have another letter prefixed.  Example: atomic
cut is ai^, super atomic cut is sai^.