Revision #1 Authors: Arnold Beckmann, Pavel Pudlak, Neil Thapen

Accepted on: 21st June 2013 09:29

Downloads: 2892

Keywords:

A propositional proof system is \emph{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 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 in

P, the games in which the first player has a positional strategy

from the games in which the second player has a positional winning

strategy.

Our main technique is to show that a suitable weak bounded

arithmetic theory proves that both players in a game cannot

simultaneously have a winning strategy, and then to translate this

proof into propositional form.

TR13-092 Authors: Pavel Pudlak, Arnold Beckmann, Neil Thapen

Publication: 19th June 2013 10:31

Downloads: 2774

Keywords:

A propositional proof system is \emph{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 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 in

P, the games in which the first player has a positional strategy

from the games in which the second player has a positional winning

strategy.

Our main technique is to show that a suitable weak bounded

arithmetic theory proves that both players in a game cannot

simultaneously have a winning strategy, and then to translate this

proof into propositional form.