Conflict nets
Conflict nets
复制标题
冲突网
DOI：
10.1145/2933575.2934559
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Hughes D
中科院分区：
文献类型：
--
作者：
Hughes D
MLL（无单位乘法线性逻辑）和ALL（无单位加性线性逻辑）的证明网是证明的图形抽象，它们是有效的（证明在线性时间内转换）和规范的（规则交换下不变的）。本文解决了一个持续了三十年的开放性问题：对于MALL（无单位乘加线性逻辑）是否存在有效的规范证明网络？考虑到MLL和ALL正则性，其中所有交换都是严格的局部证明树重写，我们定义了MALL的局部正则性：局部规则交换下的不变性。我们提出了一种新的证明网络，称为冲突网，它既有效又具有本地规范。
Proof nets for MLL (unit-free multiplicative linear logic) and ALL (unit-free additive linear logic) are graphical abstractions of proofs which are efficient (proofs translate in linear time) and canonical (invariant under rule commutation). This paper solves a three-decade open problem: are there efficient canonical proof nets for MALL (unit-free multiplicative-additive linear logic)?Honouring MLL and ALL canonicity, in which all commutations are strictly local proof-tree rewrites, we define local canonicity for MALL: invariance under local rule commutation. We present new proof nets for MALL, called conflict nets, which are both efficient and locally canonical.