Algebraic proofs over noncommutative formulas

0374819 - MÚ 2012 RIV US eng J - Článek v odborném periodiku
Tzameret, Iddo
Algebraic proofs over noncommutative formulas.
Information and Computation. Roč. 209, č. 10 (2011), s. 1269-1292. ISSN 0890-5401. E-ISSN 1090-2651
Grant CEP: GA MŠMT LC505
Výzkumný záměr: CEZ:AV0Z10190503
Klíčová slova: proof complexity * algebraic proof systems * frege proofs
Kód oboru RIV: BA - Obecná matematika
Impakt faktor: 0.560, rok: 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.
Trvalý link: http://hdl.handle.net/11104/0207646