非交换公式上的代数证明
摘要：非交换公式的代数命题证明系统的可能形式研究。我们观察到，一个简单的表达形式至少产生与Frege一样强大的系统——提供了一种语义方式来定义Cook-Reckhow（即多项式可验证的）Frege证明的代数模拟，不同于[BIKPRS96，GH03]中给出的模拟。然后我们转向一个明显较弱的系统，即多项式演算（PC），其中多项式被写作有序公式（简称有序公式的PC）：有序多项式是非交换多项式，其中每个单项式中的乘积顺序遵守变量上的固定线性顺序；代数公式是有序的，如果由它的每个子公式计算的多项式是有序的。我们展示了有序公式的PC比resolution、多项式演算和多项式演算与resolution（PCR）更强，并且对鸽巢原理和Tseitin公式具有多项式大小的证明。最后，我们提出了一种基于非交换公式上的下界特性来建立有序公式的PC证明和相关系统的下界的方法。本工作的动机是发展一种技术，将秩论证（类似于在代数电路复杂性中使用的技术）纳入命题证明的下界证明中。
作者：Iddo Tzameret
论文ID：1004.2159
分类：Computational Complexity
分类简称：cs.CC
提交时间：2010-08-03