Resolution by pebbling games
Seminar Room 1, Newton Institute
We present an approach to study the complexity of refutations in Resolution by means of certain pebbling games. We will define certain classes of such games that allow to obtain a new frame for: (1) proving size lower bounds in Resolution; (2) devising new algorithms to find Resolution refutations; (3) characterizing the hardness of provability in Resolution as an "almost" satisfiability. We'll discuss about how to extend a similar approach to stronger systems than Resolution.