  An important normal form theorem for the structure of cut-free proofs was provided by Andreoli  (1992). He classified a non-atomic formula as asynchronous if its top-level logical connective is \(\top\), &amp;, \(\bot , \lpar\), \(\quest\), or \(\forall\) or synchronous if its top-level logical connective is \(0, \oplus , 1, \otimes\), \(\bang\), or \(\exists\).