论文标题
重新审视有限模型理论和证据复杂性：在无选多项式时间和扩展多项式演算中区分图形
Finite Model Theory and Proof Complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
论文作者
论文摘要
本文从有限模型理论和命题/代数证明系统中扩展了有关逻辑之间的联系的先前工作。我们表明，如果可以通过计数（CPT）在给定图类类中的所有非同构图在逻辑中的多项式时间（CPT）中进行区分，那么它们也可以在有界扩展的多项式计算（EPC）中进行区分，并且驳斥的大小与CPT-Sentence的资源大小相同。这允许将EPC的下限传递到CPT，因此构成了更好地理解CPT极限的新潜在方法。图形同构问题的PTIME-INSANCE的超级多项式EPC下限将与PTIME分开，从而解决了有限模型理论中的一个主要开放问题。此外，使用我们的结果，我们提供了一个模型的理论证明，用于分离有界多项式的积分和有界度的扩展多项式计算。
This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the limits of CPT. A super-polynomial EPC lower bound for a PTIME-instance of the graph isomorphism problem would separate CPT from PTIME and thus solve a major open question in finite model theory. Further, using our result, we provide a model theoretic proof for the separation of bounded-degree polynomial calculus and bounded-degree extended polynomial calculus.
