一句话：证明 Frobenius 伪幺半群与 snakeorator 的相干性，并由此给出非对称乘法线性逻辑证明的三维几何记法。
这篇论文研究 monoidal 双范畴中 Frobenius 伪幺半群与 snakeorator 的相干性，并将其应用于非对称乘法线性逻辑的证明表示。作者证明相应的相干定理，由此为线性逻辑证明构造三维图式，同时引入几何等价来刻画证明之间的等价关系。得到的 3D 记法不需要全局正确性判据，也不需要 thinning links，这与传统 proof nets 的表示方式形成对比。论文进一步论证传统 proof nets 可看作这些三维图式的二维投影，从而用更高维几何统一理解线性证明的结构与等价。
We prove coherence theorems for Frobenius pseudomonoids and snakeorators in monoidal bicategories. As a consequence we obtain a 3d notation for proofs in nonsymmetric multiplicative linear logic, with a geometrical notion of equivalence, and without the need for a global correctness criterion or thinning links. We argue that traditional proof nets are the 2d projections of these 3d diagrams.
@article{paperbot780,
title = {Coherence for Frobenius pseudomonoids and the geometry of linear proofs},
author = {Lawrence Dunn and Jamie Vicary},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:5)2019}
}