Proof nets for unit-free multiplicative-additive linear logic
Proof nets for unit-free multiplicative-additive linear logic
复制标题
无单位乘加线性逻辑的证明网
DOI：
10.1145/1094622.1094629
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
R. V. Glabbeek
中科院分区：
文献类型：
--
作者：
Dominic J. D. Hughes;R. V. Glabbeek
无单位乘法线性逻辑（MLL）证明网理论的基石是模非本质规则交换的无割证明的抽象表示。唯一已知的基于单项权重的加法器扩展未能保持这一关键功能：大量的无割单项证明网可以对应于相同的无割证明。因此，自1986年线性逻辑诞生以来，为无单位乘加线性逻辑（MALL）找到一个令人满意的证明网概念的问题一直没有解决。我们提出了一个新的定义MALL证明网仍然忠实于MLL理论的基石。
A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential rule commutation. The only known extension to additives, based on monomial weights, fails to preserve this key feature: a host of cut-free monomial proof nets can correspond to the same cut-free proof. Thus, the problem of finding a satisfactory notion of proof net for unit-free multiplicative-additive linear logic (MALL) has remained open since the inception of linear logic in 1986. We present a new definition of MALL proof net which remains faithful to the cornerstone of the MLL theory.