Parity Games and Propositional Proofs
From MaRDI portal
Publication:5169973
DOI10.1145/2579822zbMath1291.03111OpenAlexW1966303481MaRDI QIDQ5169973
Arnold Beckmann, Neil Thapen, Pavel Pudlák
Publication date: 17 July 2014
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2579822
parity gamesresolutionbounded arithmeticmean payoff gamesweak automatizabilitysimple stochastic sames
Stochastic games, stochastic differential games (91A15) Mechanization of proofs and logical operations (03B35) Combinatorial games (91A46) Complexity of proofs (03F20)
Related Items
Short refutations for an equivalence‐chain principle for constant‐depth formulas, The canonical pairs of bounded depth Frege systems, INCOMPLETENESS IN THE FINITE DOMAIN, The treewidth of proofs
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Mean-payoff games and propositional proofs
- Positional strategies for mean payoff games
- The complexity of stochastic games
- The complexity of mean payoff games on graphs
- On reducibility and symmetry of disjoint NP pairs.
- Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems
- Non-automatizability of bounded-depth Frege proofs
- On the automatizability of resolution and related propositional proof systems
- On the weak pigeonhole principle
- Automatizability and Simple Stochastic Games
- The provably total search problems of bounded arithmetic
- Recursive algorithm for parity games requires exponential time
- An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- Bounded existential induction
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Short proofs are narrow—resolution made simple
- NP search problems in low fragments of bounded arithmetic
- Stochastic Games
