Algebraic proofs over noncommutative formulas

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F11%3A00374819" target="_blank" >RIV/67985840:_____/11:00374819 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.ic.2011.07.004" target="_blank" >http://dx.doi.org/10.1016/j.ic.2011.07.004</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.ic.2011.07.004" target="_blank" >10.1016/j.ic.2011.07.004</a>

Result language
angličtina
Original language name
Algebraic proofs over noncommutative formulas
Original language description
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 thelinear order, than the variables in the right subformula of the gate.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
BA - General mathematics
OECD FORD branch
—

Project
<a href="/en/project/LC505" target="_blank" >LC505: Eduard Čech Center for Algebra and Geometry</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)

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

Similar results(10)