一句话：证明 pomset 逻辑与 BV 并不相同，并确定二者可证性复杂度分别达 Σ₂^p-完全与 NP-完全。
pomset 逻辑与 BV 都是在带 Mix 的乘法线性逻辑上加入一个自对偶、非交换连接词而得到的逻辑。前者源于相干空间与证明网研究，后者源于 series-parallel order、cograph 与证明系统。两者都有切割可消去性，但均不能在序贯演算中直接处理：pomset 逻辑的可证性可通过证明网正确性准则判定，BV 则可用深推理证明系统刻画。长期以来人们猜想这两个逻辑相同。本文否证该猜想，并研究二者的可证性复杂度，发现存在巨大差距：BV 的可证性是 NP-完全的，而 pomset 逻辑的可证性是 Σ₂^p-完全的。文章还对二者可能的序贯系统作出一些观察。
Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same. In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in pomset logic is $\Sigma_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.
@article{paperbot2165,
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 = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:25)2023}
}