非交换公式的代数证明
Algebraic Proofs over Noncommutative Formulas
摘要：
我们研究了代数命题证明系统与非交换公式操作的可能配方。我们观察到，一个简单的公式产生了至少像弗雷格一样强大的系统-产生了一种语义方式来定义一个Cook-Reckhow（即，多项式验证）代数模拟弗雷格证明，不同于[BIKPRS 96，GH 03]。然后，我们转向一个明显较弱的系统，即多项式演算（PC），其中多项式被写为有序公式（PC over ordered formulas，简称）：有序多项式是一个非交换多项式，其中每个单项式中的乘积的顺序都是变量的固定线性顺序;如果由每个子公式计算的多项式是有序的，则代数公式是有序的。我们表明，PC有序公式是严格强于决议，多项式演算和多项式演算与决议（PCR），并承认多项式大小反驳鸽子洞原则和Tseitin的公式。最后，我们提出了一种方法，建立下界PC上的顺序公式证明，和相关的系统，根据非交换公式的下界的性质。这项工作背后的动机是开发技术，将秩参数（类似于代数电路复杂性中使用的）建立命题证明的下限。
英文摘要：
We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege---yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in [BIKPRS96,GH03]. We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short): an ordered polynomial is a noncommutative polynomial in which the order of products in every monomial respects a fixed linear order on variables; an algebraic formula is ordered if the polynomial computed by each of its subformulas is ordered. We show that PC over ordered formulas is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR) and admits polynomial-size refutations for the pigeonhole principle and the Tseitin's formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas. The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in algebraic circuit complexity) for establishing lower bounds on propositional proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
