Algebraic proofs over noncommutative formulas

0374819 - MÚ 2012 RIV US eng J - Journal Article
Tzameret, Iddo
Algebraic proofs over noncommutative formulas.
Information and Computation. Roč. 209, č. 10 (2011), s. 1269-1292. ISSN 0890-5401. E-ISSN 1090-2651
R&D Projects: GA MŠMT LC505
Institutional research plan: CEZ:AV0Z10190503
Keywords : proof complexity * algebraic proof systems * frege proofs
Subject RIV: BA - General Mathematics
Impact factor: 0.560, year: 2011
http://www.sciencedirect.com/science/article/pii/S089054011100109X

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 Buss et al. (1997) and Grigoriev and Hirsch (2003). 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). Given some fixed linear order on variables, an arithmetic formula is ordered if for each of its product gates the left subformula contains only variables that are less-than or equal, according to the linear order, than the variables in the right subformula of the gate.
Permanent Link: http://hdl.handle.net/11104/0207646