. "185175" . "10" . . "Information and Computation and Information and Control" . . . "Algebraic proofs over noncommutative formulas"@en . "24"^^ . . . "Algebraic proofs over noncommutative formulas" . "Tzameret, Iddo" . . "000295019700001" . . . "[021CDBFFAFFE]" . . . "Tzameret, Iddo" . . "Algebraic proofs over noncommutative formulas"@en . . . "209" . "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."@en . "0890-5401" . "RIV/67985840:_____/11:00374819!RIV12-AV0-67985840" . . . "Algebraic proofs over noncommutative formulas" . "1"^^ . . "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." . "P(LC505), Z(AV0Z10190503)" . "10.1016/j.ic.2011.07.004" . "proof complexity; algebraic proof systems; frege proofs"@en . "1"^^ . "US - Spojen\u00E9 st\u00E1ty americk\u00E9" . "RIV/67985840:_____/11:00374819" .