交互和结构的系统III：BV和Pomset逻辑的复杂性
摘要：Pomset逻辑与BV逻辑都是将混合线性逻辑（含混合）扩展为第三个连接词的逻辑，这个连接词是自对偶且非可交换的。Pomset逻辑起源于相关空间和证明网的研究，BV逻辑起源于串并行序、卡夫图和证明系统的研究。这两个逻辑都具有剪切可证明性结果，但对于任何逻辑，这都无法在序列演算中完成。Pomset逻辑的可证明性可以通过证明网正确性标准进行检查，而BV逻辑可以通过深层推理证明系统进行检查。长期以来一直有人猜测这两个逻辑是相同的。本文证明了这个猜想是错误的。我们还研究了这两个逻辑的复杂性，并展示了它们之间的巨大差距。在BV逻辑中的可证明性是NP完全的，在Pomset逻辑中的可证明性是$Sigma\_2^p$完全的。我们还就两个逻辑的可能序列系统进行了一些观察。
作者：L^e Th`anh D~ung Nguy^en and Lutz Stra{ss}burger
论文ID：2209.07825
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-06