论文标题
互动与结构系统III：BV和POMSET逻辑的复杂性
A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
论文作者
论文摘要
POMET逻辑和BV都是逻辑，它们具有乘法线性逻辑（混合），并具有第三个结节，该连接是自偶，不交流的。 POMET逻辑源自对相干空间和证明网的研究，而BV源自对串联平行订单，cographs和Proof Systems的研究。两种逻辑都均获得了可行性的结果，但是对于这两个逻辑都不能在依次的微积分中完成。可以通过证明网络正确性标准和BV中的POMSET逻辑中的Provability通过深层推理系统检查。长期以来，人们一直认为这两个逻辑是相同的。 在本文中，我们表明这个猜想是错误的。我们还研究了两种逻辑的复杂性，在两者之间表现出巨大的差距。尽管BV中的可储实性是NP完整的，而POMSET逻辑中的Provibaly为$σ_2^p $ -complete。我们还对两种逻辑的可能序列系统进行了一些观察。
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 $Σ_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.
