Algebraic proofs over noncommutative formulas

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F10%3A00374767" target="_blank" >RIV/67985840:_____/10:00374767 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Algebraic proofs over noncommutative formulas
Original language description
We study possible formulations of algebraic propositional proofs operating with noncommutative polynomials written as algebraic noncommutative formulas. First, we observe that a simple formulation of such proof systems gives rise to systems at least as strong as Frege-yielding also a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic variant of Frege proofs, different from that given before in [8,11]. 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 ordering 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
Czech name
—
Czech description
—

Publication year
2010
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)