This HTML5 document contains 41 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n16http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F67985840%3A_____%2F11%3A00374819%21RIV12-AV0-67985840/
n11http://linked.opendata.cz/resource/domain/vavai/projekt/
n18http://linked.opendata.cz/resource/domain/vavai/subjekt/
n5http://linked.opendata.cz/ontology/domain/vavai/
n10http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n19http://bibframe.org/vocab/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n17http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n6http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n13http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F67985840%3A_____%2F11%3A00374819%21RIV12-AV0-67985840
rdf:type
n5:Vysledek skos:Concept
dcterms: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 the linear order, than the variables in the right subformula of the gate. 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 the linear order, than the variables in the right subformula of the gate.
dcterms:title
Algebraic proofs over noncommutative formulas Algebraic proofs over noncommutative formulas
skos:prefLabel
Algebraic proofs over noncommutative formulas Algebraic proofs over noncommutative formulas
skos:notation
RIV/67985840:_____/11:00374819!RIV12-AV0-67985840
n5:predkladatel
n18:ico%3A67985840
n3:aktivita
n6:P n6:Z
n3:aktivity
P(LC505), Z(AV0Z10190503)
n3:cisloPeriodika
10
n3:dodaniDat
n13:2012
n3:domaciTvurceVysledku
Tzameret, Iddo
n3:druhVysledku
n9:J
n3:duvernostUdaju
n12:S
n3:entitaPredkladatele
n16:predkladatel
n3:idSjednocenehoVysledku
185175
n3:idVysledku
RIV/67985840:_____/11:00374819
n3:jazykVysledku
n4:eng
n3:klicovaSlova
proof complexity; algebraic proof systems; frege proofs
n3:klicoveSlovo
n17:algebraic%20proof%20systems n17:proof%20complexity n17:frege%20proofs
n3:kodStatuVydavatele
US - Spojené státy americké
n3:kontrolniKodProRIV
[021CDBFFAFFE]
n3:nazevZdroje
Information and Computation and Information and Control
n3:obor
n14:BA
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
1
n3:projekt
n11:LC505
n3:rokUplatneniVysledku
n13:2011
n3:svazekPeriodika
209
n3:tvurceVysledku
Tzameret, Iddo
n3:wos
000295019700001
n3:zamer
n10:AV0Z10190503
s:issn
0890-5401
s:numberOfPages
24
n19:doi
10.1016/j.ic.2011.07.004