A System of Interaction and Structure II: The Need for Deep Inference

Alwen Tiu

This paper studies properties of the logic BV, which is an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. BV is presented in the calculus…