About: Algebraic proofs over noncommutative formulas

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Algebraic proofs over noncommutative formulas Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
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. (en)
Title	Algebraic proofs over noncommutative formulas Algebraic proofs over noncommutative formulas (en)
skos:prefLabel	Algebraic proofs over noncommutative formulas Algebraic proofs over noncommutative formulas (en)
skos:notation	RIV/67985840:_____/11:00374819!RIV12-AV0-67985840
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(LC505), Z(AV0Z10190503)
http://linked.open...iv/cisloPeriodika	10
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Tzameret, Iddo
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Matematický ústav AV ČR, v. v. i.
http://linked.open...dnocenehoVysledku	185175
http://linked.open...ai/riv/idVysledku	RIV/67985840:_____/11:00374819
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	proof complexity; algebraic proof systems; frege proofs (en)
http://linked.open.../riv/klicoveSlovo	algebraic proof systems frege proofs proof complexity
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[021CDBFFAFFE]
http://linked.open...i/riv/nazevZdroje	Information and Computation and Information and Control
http://linked.open...in/vavai/riv/obor	BA
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	1 (xsd:int)
http://linked.open...vavai/riv/projekt	Eduard Čech Center for Algebra and Geometry
http://linked.open...UplatneniVysledku	2011
http://linked.open...v/svazekPeriodika	209
http://linked.open...iv/tvurceVysledku	Tzameret, Iddo
http://linked.open...ain/vavai/riv/wos	000295019700001
http://linked.open...n/vavai/riv/zamer	Rozvoj a prohloubení obecných matematických poznatků a jejich užití v dalších vědních oborech a v praxi
issn	0890-5401
number of pages	24 (xsd:int)
http://bibframe.org/vocab/doi	10.1016/j.ic.2011.07.004

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 77 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software