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.

翻译：Pomset逻辑与BV均是扩展乘法线性逻辑（含Mix）的逻辑体系，二者引入了一种自对偶且非交换的第三连接词。Pomset逻辑源于相干空间与证明网的研究，而BV则源自串并联序、余图及证明系统的探索。两种逻辑均具备切割可容许性，但无法在相继式演算中实现。Pomset逻辑的可证明性可通过证明网正确性准则检验，BV则依赖深层推理证明系统。长期以来，学界猜测这两种逻辑等价，但本文证明此猜想不成立。我们同时探究两种逻辑的复杂性，发现二者存在显著差异：BV的可证明性为NP完全问题，而Pomset逻辑的可证明性则为$\Sigma_2^p$完全问题。此外，本文还对两种逻辑可能的相继式系统进行了相关讨论。