Parity games and propositional proofs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F13%3A00422131" target="_blank" >RIV/67985840:_____/13:00422131 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-642-40313-2_12" target="_blank" >http://dx.doi.org/10.1007/978-3-642-40313-2_12</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-40313-2_12" target="_blank" >10.1007/978-3-642-40313-2_12</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Parity games and propositional proofs
Popis výsledku v původním jazyce
A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which 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 also define a 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.
Název v anglickém jazyce
Parity games and propositional proofs
Popis výsledku anglicky
A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which 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 also define a 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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
BA - Obecná matematika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/IAA100190902" target="_blank" >IAA100190902: Matematická logika, složitost a algoritmy</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2013
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Mathematical Foundations of Computer Science 2013
ISBN
978-3-642-40312-5
ISSN
—
e-ISSN
—
Počet stran výsledku
12
Strana od-do
111-122
Název nakladatele
Springer
Místo vydání
Berlin
Místo konání akce
Klosterneuburg
Datum konání akce
26. 8. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—