论文标题：命题证明复杂性的有限模型理论观点
摘要：命题证明复杂性与有限模型论之间建立了新的和令人惊讶的紧密联系。具体而言，我们表明几个命题证明系统，如Horn分辨率、有界宽度分辨率和有界次数的单项式演算，可以以精确的方式通过描述性复杂度理论中的固定点逻辑变体来描述其能力。我们的主要结果是Horn分辨率与最小固定点逻辑具有相同的表达能力，有界宽度分辨率捕捉到存在最小固定点逻辑，且有有界次数的多项式演算器能够解决精确叙述性复杂度理论中固定点逻辑的问题。我们还研究了有界次数的多项式演算。对于有理数，如果我们限制系数的位复杂性，它能够捕捉到具有计数的固定点逻辑。对于无限制的系数，我们只能说有界次数的多项式演算至多与有界变量无穷计数逻辑具有相同的能力，但其能力的精确逻辑特征仍然是一个悬而未决的问题。这些逻辑与证明系统之间的联系使我们能够建立用于证明有理数上和有限域上多项式演算的下界的有限模型理论工具。 这是在2019年1月23日最初发布的论文(arXiv:1802.09377)的修正版本。
作者：Erich Gr"adel and Martin Grohe and Benedikt Pago and Wied Pakusa
论文ID：1802.09377
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22