2025/06/26 by Raffaele Di Donna, Lorenzo Tortora de Falco, Di Donna, Raffaele +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2506.21678
openalex publication_date 2025/06/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.