线性逻辑中独特的完美匹配、禁止转换和证明网格
摘要：线性逻辑与主流图论之间建立了一座桥梁，建立在Retor''e（2003年）的基础上。我们证明了MLL+Mix证明网的正确性问题与完美匹配的唯一性问题等价。通过应用匹配理论，我们获得了MLL+Mix证明网的新结果：线性时间正确性标准、准线性的顺序化算法以及对正确性问题的次多项复杂性的刻画。我们还将图算法应用于计算Bagnol等人（2015年）的依赖关系和Bellin（1997年）的王国排序，并将它们与组合最大匹配算法的关键概念“花”联系起来。 在本期刊版本中，我们根据具有禁止转换的图的一般构造，对Retor''e的“RB图”进行了解释。事实上，正是通过分析RB图，我们得到了一种在多项式时间内找到避免禁止转换的路径的算法；后者是作者关注的另一篇专注于图论的论文（arXiv:1901.07028）中涵盖的内容之一。
作者：L^e Th`anh D~ung Nguy^en
论文ID：1901.10247
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22