Journal article 1166 views
Parity Games and Propositional Proofs
,
Pavel Pudlák,
Neil Thapen
ACM Transactions on Computational Logic, Volume: 15, Issue: 2, Pages: 17:1 - 17:30
Swansea University Author:
Arnold Beckmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1145/2579822
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...
| Published in: | ACM Transactions on Computational Logic |
|---|---|
| Published: |
2014
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa17523 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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 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 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. |
|---|---|
| Keywords: |
Bounded arithmetic, mean payoff games, parity games, resolution, simple stochastic sames, weak automatizability |
| College: |
Faculty of Science and Engineering |
| Issue: |
2 |
| Start Page: |
17:1 |
| End Page: |
17:30 |