一句话：该文将 MLL+Mix 证明网正确性归约为完美匹配唯一性，并由此给出线性时间判定与准线性顺序化算法。
本文在 Retoré（2003）的基础上建立线性逻辑与图论之间的桥梁。核心结果是：MLL+Mix 证明网的正确性问题等价于完美匹配的唯一性问题。借助匹配理论，作者得到线性时间的正确性判定准则、准线性的顺序化算法，并刻画了正确性问题的亚多项式复杂度。论文还用图算法计算 Bagnol 等（2015）的依赖关系与 Bellin（1997）的 kingdom 序，并将其与最大匹配中的 blossom 概念关联。期刊版新增了用带禁止转移的图的一般构造解释 Retoré 的 RB-graphs，并由此得到寻找避开禁止转移的 trail 的多项式时间算法。
This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retor\'e (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms. In this journal version, we have added an explanation of Retor\'e's "RB-graphs" in terms of a general construction on graphs with forbidden transitions. In fact, it is by analyzing RB-graphs that we arrived at this construction, and thus obtained a polynomial-time algorithm for finding trails avoiding forbidden transitions; the latter is among the material covered in another paper by the author focusing on graph theory (arXiv:1901.07028).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Nguyen19,
title = {Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix},
author = {Lê Thành Dũng Nguyên},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:27)2020}
}