重访有限模型理论与证明复杂性：在无选择多项式时间中区分图与扩展多项式演算
计算机科学中的逻辑
2023-02-13 v3 计算复杂性
摘要
本文扩展了先前关于有限模型理论中的逻辑与命题/代数证明系统之间联系的工作。我们证明，如果在给定图类中的所有非同构图都能在无选择多项式时间带计数逻辑（CPT）中被区分，那么它们也能在有限度扩展多项式演算（EPC）中被区分，且反驳的大小与 CPT 句子的资源消耗大致相同。这允许将 EPC 的下界转移到 CPT，从而构成理解 CPT 局限性的新的潜在途径。图同构问题的一个 PTIME 实例的超多项式 EPC 下界将把 CPT 与 PTIME 分离，从而解决有限模型论中的一个主要开放问题。此外，利用我们的结果，我们提供了有限度多项式演算与有限度扩展多项式演算分离的模理论证明。
引用
@article{arxiv.2206.05086,
title = {Finite Model Theory and Proof Complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus},
author = {Benedikt Pago},
journal= {arXiv preprint arXiv:2206.05086},
year = {2023}
}
备注
Full version of a paper to appear at CSL 2023