一句话：提出消除存在量词见证冗余的 MLL1 规范证明网——合一证明网。
MLL（无单位乘法线性逻辑）的证明网是证明的简洁图形表示，能够抽象掉非交互规则顺序等语法冗余，因而具有规范性。作者指出，Girard 对 MLL1（一阶 MLL）的扩展由于存在量词见证的冗余而不具备规范性。为此，论文提出称为合一证明网的 MLL1 规范证明网，其中不存在被指定的见证。以 ∀x Px ⊢ ∃x Px 为例：Girard 网有无穷多个无割证明，分别对应 ∃x 的任意见证；而合一证明网只有一个无割且未指定见证的证明。
Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard's extension to MLL1 (first-order MLL) fails to be canonical because of redundant existential witnesses, and present canonical MLL1 proof nets called unification nets without them. For example, while there are infinitely many cut-free Girard nets ∀x Px ⊢ ∃x Px, one per arbitrary witness for ∃x, there is a unique cut-free unification net, with no specified witness.
DOI 原文 ·
@inproceedings{paperbot4334,
title = {Unification nets},
author = {Dominic J. D. Hughes},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209159}
}