Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Pinyin
i2Cantonese
i2Cangjie
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TAMC

2010

Springer

2010

Springer

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 deﬁne a CookReckhow (i.e., polynomially veriﬁable) algebraic analogue of Frege proofs, diﬀerent 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 ﬁxed 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...

Related Content

Added |
11 Jul 2010 |

Updated |
11 Jul 2010 |

Type |
Conference |

Year |
2010 |

Where |
TAMC |

Authors |
Iddo Tzameret |

Comments (0)