We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting.

翻译：本文研究了一种扩展Danos-Regnier线性逻辑证明结构正确性判定的性质。该性质适用于证明结构的正确性图：它断言任何此类图均为无环图，且其连通分量数恰好比底部节点或弱化节点数多一。众所周知，在乘性指数线性逻辑中，该性质是从证明结构恢复相继式演算证明的必要非充分条件。我们提出未类型化证明结构的几何条件，使得这一必要性质可转化为充分条件：由此可分离出该性质确实构成正确性判定的线性逻辑片段。在带单位的乘性线性逻辑的适当片段中，该判定准则可刻画相继式演算规则置换所诱导的等价关系。在直觉主义线性逻辑中，该性质等价于仅有一个输出结论的常见要求，且在无公理设定下足以实现序列化。