A new correctness criterion for multiplicative non-commutative proof nets
A new correctness criterion for multiplicative non-commutative proof nets
复制标题
乘法非交换证明网的新正确性准则
DOI：
--
复制
发表时间：
2003
影响因子：
0.3
通讯作者：
Roberto Maieli
中科院分区：
文献类型：
--
作者：
Roberto Maieli
摘要。我们引入了一个新的乘法非交换证明网的正确性判据，该判据可以看作是线性逻辑证明网的Danos-Regnier判据的非交换对偶。主要的直觉依赖于这样一个事实，即证明网的任何切换（通过破坏每个分离环节的一个前提而获得）可以自然地视为证明网结论上的串并联顺序变化（循环关系）。
Abstract. We introduce a new correctness criterion for multiplicative non commutative proof nets which can be considered as the non-commutative counterpart to the Danos-Regnier criterion for proof nets of linear logic. The main intuition relies on the fact that any switching for a proof net (obtained by mutilating one premise of each disjunction link) can be naturally viewed as a series-parallel order variety (a cyclic relation) on the conclusions of the proof net.