### arnold beckmann's pages

## Parity Games and Propositional Proofs

**File:** PDF-File

**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,
Klosterneuburg, Austria,
August 26-30, 2013. LNCS 8087.

**Pages:** 111-122

**DOI:** 10.1007/978-3-642-40313-2_12

**Abstract:**
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.