arnold beckmann's pages
Parity Games and Propositional Proofs
Author: Arnold Beckmann, Pavel Pudlák and Neil Thapen
Title: Parity Games and Propositional Proofs
Proceedings: 38th International Symposium on
Mathematical Foundations of Computer Science, MFCS 2013,
August 26-30, 2013. LNCS 8087.
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.