A characterization of tree-like Resolution size ?
We explain an asymmetric ProverDelayer game which precisely characterizes proof size in tree-like Resolution. Our proof method allows to always achieve the optimal lower bounds. Intuitive information-theoretic interpretation of the game.
resolution proverdelayer games computational complexity proof complexity