交互与结构系统 III：BV 与 Pomset 逻辑的复杂性
计算机科学中的逻辑
2024-02-14 v5
摘要
Pomset 逻辑与 BV 均为在乘性线性逻辑（含 Mix）基础上扩展出自对偶且非交换的第三连接词的logic。Pomset 逻辑源于相干空间与证明网的研究，而 BV 源于串并行序、余图与证明系统的研究。两种逻辑均具有切割可容许性结果，但均无法在相继式演算中实现。Pomset 逻辑的可证性可通过证明网正确性判据检验，BV 的可证性可通过深度推理证明系统检验。长期以来人们猜想这两种逻辑相同。本文表明该猜想不成立。我们还研究了两种逻辑的复杂性，揭示了二者间的巨大差距：BV 的可证性为 NP 完全，而 Pomset 逻辑的可证性为 -完全。我们还对两种逻辑可能的相继式系统作了若干观察。
引用
@article{arxiv.2209.07825,
title = {A System of Interaction and Structure III: The Complexity of BV and Pomset Logic},
author = {Lê Thành Dũng Nguyên and Lutz Straßburger},
journal= {arXiv preprint arXiv:2209.07825},
year = {2024}
}