Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the standard sequent calculus one, provide a simplified translation, and provide a formal proof that a standard approach to modelling is indeed invariant to all these translations. En route we establish a necessary condition for provable sequents related to the number of pars and tensors in a formula that seems to be missing from the literature.

翻译：乘法线性逻辑是一个被广泛研究的形式系统，大多数此类研究关注于单边相继式演算。本文详细考察了深度推理系统与标准相继式演算之间的现有转换关系，提出了一种简化的转换方法，并给出了一个形式化证明——标准建模方法实际上对所有这类转换都是不变的。在此过程中，我们建立了一个与公式中"par"和"张量"数量相关的可证明相继式必要条件，这一条件在现有文献中似乎尚未被记载。