Algebraic proofs over noncommutative formulas

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Algebraic proofs over noncommutative formulas

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Algebraic proofs over noncommutative formulas

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

<a href="/cs/project/LC505" target="_blank" >LC505: Centrum Eduarda Čecha pro algebru a geometrii</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2011

Kód důvěrnosti údajů

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

Název periodika

Information and Computation and Information and Control

ISSN

0890-5401

e-ISSN

—

Svazek periodika

209

Číslo periodika v rámci svazku

10

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

24

Strana od-do

1269-1292

Kód UT WoS článku

000295019700001

EID výsledku v databázi Scopus

—