About: Parity games and propositional proofs

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

About: Parity games and propositional proofs 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	A propositional proof system is weakly automatizable if there is a polynomial time algorithm that separates satisfiable formulas from formulas that have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. A propositional proof system is weakly automatizable if there is a polynomial time algorithm that separates satisfiable formulas from formulas that have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. (en)
Title	Parity games and propositional proofs Parity games and propositional proofs (en)
skos:prefLabel	Parity games and propositional proofs Parity games and propositional proofs (en)
skos:notation	RIV/67985840:_____/14:00430389!RIV15-AV0-67985840
http://linked.open...avai/riv/aktivita	I P
http://linked.open...avai/riv/aktivity	I, P(IAA100190902)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2015
http://linked.open...aciTvurceVysledku	Thapen, Neil Pudlák, Pavel
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	35778
http://linked.open...ai/riv/idVysledku	RIV/67985840:_____/14:00430389
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	bounded arithmetic; mean payoff games; parity games (en)
http://linked.open.../riv/klicoveSlovo	parity games bounded arithmetic mean payoff games
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[171B7463D81B]
http://linked.open...i/riv/nazevZdroje	ACM Transactions on Computational Logic
http://linked.open...in/vavai/riv/obor	BA
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Mathematical logic, complexity, and algorithms
http://linked.open...UplatneniVysledku	2014
http://linked.open...v/svazekPeriodika	15
http://linked.open...iv/tvurceVysledku	Thapen, Neil Pudlák, Pavel Beckmann, A.
http://linked.open...ain/vavai/riv/wos	000336005000007
issn	1529-3785
number of pages	30 (xsd:int)
http://bibframe.org/vocab/doi	10.1145/2579822

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, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software