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.

websites: Arnold Beckmann 2017-08-28 Valid HTML 4.01! Valid CSS!