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$完全的。此外，本文针对这两种逻辑可能的相继式系统提出了一些观察结论。