Algebraic Proofs over Noncommutative Formulas

9 years 3 months ago
Algebraic Proofs over Noncommutative Formulas
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 CookReckhow (i.e., polynomially verifiable) algebraic analogue of Frege proofs, different from that given in [BIK+ 97, 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). 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 t...
Iddo Tzameret
Added 11 Jul 2010
Updated 11 Jul 2010
Type Conference
Year 2010
Where TAMC
Authors Iddo Tzameret
Comments (0)