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_____%2F10%3A00374767" target="_blank" >RIV/67985840:_____/10:00374767 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

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

Název v anglickém jazyce

Algebraic proofs over noncommutative formulas

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2010

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 statě ve sborníku

Theory and Applications of Models of Computation

ISBN

978-3-642-13561-3

ISSN

—

e-ISSN

—

Počet stran výsledku

12

Strana od-do

60-71

Název nakladatele

Springer

Místo vydání

Berlin

Místo konání akce

Prague,

Datum konání akce

7. 6. 2010

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000279560400006