ECCC-Report TR10-097https://eccc.weizmann.ac.il/report/2010/097Comments and Revisions published for TR10-097en-usMon, 02 Aug 2010 13:24:06 +0300
Revision 1
| Algebraic Proofs over Noncommutative Formulas |
Iddo Tzameret
https://eccc.weizmann.ac.il/report/2010/097#revision1We 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.Mon, 02 Aug 2010 13:24:06 +0300https://eccc.weizmann.ac.il/report/2010/097#revision1
Paper TR10-097
| Algebraic Proofs over Noncommutative Formulas |
Iddo Tzameret
https://eccc.weizmann.ac.il/report/2010/097We 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 analogue of Frege proofs, different from that given in Buss et al. [\textit{Comput. Complexity} 1995/96] and in Grigoriev and Hirsch [\textit{Theoret. Comput. Sci.} 2003]. We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (\emph{PC over ordered formulas}, for short). This is an algebraic propositional proof system that operates with noncommutative polynomials in which the order of products in all monomials respects a fixed linear order on the variables, and where proof-lines are written as noncommutative formulas. We show that the latter proof system 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.Thu, 17 Jun 2010 09:48:26 +0300https://eccc.weizmann.ac.il/report/2010/097