Proofs as Games
Mechanization of proofs and logical operations (03B35) Model theory of finite structures (03C13) Complexity of computation (including implicit computational complexity) (03D15) Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Descriptive complexity and finite models (68Q19) Applications of game theory (91A80)
Originally the exponential lower bound for propositional resolution proofs was given by \textit{A. Haken} [Theor. Comput. Sci. 39, 297-308 (1985; Zbl 0586.03010)]. The author of this article presents his own version of a proof based on a game. He shows that the space complexity of a resolution proof is equivalent to the space complexity of a winning strategy of the player Prover in the two-player pigeonhole game.
- The intractability of resolution
- A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
- Large clique is hard on average for resolution
- Partially definable forcing and bounded arithmetic
- Strong ETH and resolution via games and the multiplicity of strategies
- A game characterisation of tree-like Q-resolution size
- A characterization of tree-like resolution size
- A combinatorial characterization of resolution width
- A game characterisation of tree-like Q-resolution size
- A tradeoff between length and width in resolution
- Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
- From parity games to circular proofs
- Parity Games and Propositional Proofs
- Feasible interpolation for QBF resolution calculi
- Game Characterizations and the PSPACE-Completeness of Tree Resolution Space
- Relativization makes contradictions harder for resolution
- The limits of tractability in resolution-based propositional proof systems
- Parameterized proof complexity
- On the Descriptive Complexity of a Simplified Game of Hex
- DRAT and propagation redundancy proofs without new variables
- Short Proofs Are Hard to Find
- Resolution and the binary encoding of combinatorial principles
- Resolution lower bounds for refutation statements
- Monotone circuit lower bounds from resolution
- Parity Games and Propositional Proofs
- Narrow proofs may be maximally long
- Strong ETH and resolution via games and the multiplicity of strategies
- Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
- Theory and Applications of Satisfiability Testing
- Proof and refutation in MALL as a game
- Proof complexity and the binary encoding of combinatorial principles
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- Lower bounds for set-blocked clauses proofs
- Proving unsatisfiability with hitting formulas
- Lifting with colourful sunflowers
- On the power and limitations of branch and cut
- On exponential time lower bound of Knapsack under backtracking
This page was built for publication: Proofs as Games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2757489)
