Focusing and proof-nets in linear and non-commutative logic (Q4938434)

The paper is concerned with the so-called focalization property of proofs, widely studied in recent years [see \textit{J.-M. Andreoli} and \textit{R. Pareschi}, New Gener. Comput. 9, 445-473 (1991; Zbl 0731.68022); \textit{J.-Y. Girard}, Math. Struct. Comput. Sci. 1, No. 3, 255-296 (1991; Zbl 0752.03027); \textit{V. Danos, J.-B. Joinet} and \textit{H. Schellinx}, J. Symb. Log. 62, No. 3, 755-807 (1997; Zbl 0895.03023), and many others]. The authors notice that in the framework of multiplicative linear logic proof-nets, the focalization property can be reformulated in terms of ``hereditarily splitting'' (tensor-)links. This fact motivated them to prove the splitting lemma of \textit{J.-Y. Girard} [Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] for the proof-nets of non-commutative logic (introduced by \textit{V. M. Abrusci} and \textit{P. Ruet} [Ann. Pure Appl. Logic 101, No. 1, 29-64 (2000; Zbl 0962.03054)]), in order to extend their remarks to the non-commutative case. For the entire collection see [Zbl 0921.00037].