parity games are two player games which are played by moving a token around a finite graph. parity games have important applications in automata theory, logic, and verification - for example, the model checking problem for the modal mu-calculus is polynomial time equivalent to solving parity games. it is a long-standing open problem whether the winner in a parity game can be decided in polynomial time. in the talk, we will relate this problem to weak automatizability of resolution. 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 explain that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. this is joint work with pavel pudlak and neil thapen.