Parity games and propositional proofs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F14%3A00430389" target="_blank" >RIV/67985840:_____/14:00430389 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1145/2579822" target="_blank" >http://dx.doi.org/10.1145/2579822</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/2579822" target="_blank" >10.1145/2579822</a>

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 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 gamesin 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 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 gamesin which the second player has a positional winning strategy.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

BA - Obecná matematika

OECD FORD obor

—

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

Rok uplatnění

2014

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 periodika

ACM Transactions on Computational Logic

ISSN

1529-3785

e-ISSN

—

Svazek periodika

15

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

30

Strana od-do

—

Kód UT WoS článku

000336005000007

EID výsledku v databázi Scopus

—