Having good algorithms to verify tautologies as efficiently as possible
is of prime interest in different fields of computer science.
In this paper we present an algorithm for finding Resolution refutations
based on finding tree-like Res(k) refutations. The algorithm is based on
the one of Beame and Pitassi \cite{BP96} for tree-like Resolution, but it is
provably more efficient. On the other hand our algorithm is also
more efficient than Davis-Putnam and better in the sense of space usage than
the one of Ben-Sasson and Wigderson \cite{BSW01}.
We also analyse the possibility that a system that
simulates Resolution is automatizable. We call this notion "weak
automatizability". We prove that Resolution is weakly automatizable
if and only if Res(2) has feasible interpolation.
In order to prove this theorem, we show that Res(2) has
polynomial-size proofs of the reflection principle of Resolution
(and of any Res(k)), which is a version of consistency. We also show
that Resolution proofs of its own reflection principle require
slightly subexponential size. This gives a slightly subexponential
lower bound for the monotone interpolation of Res(2) and a
better separation from Resolution as a byproduct.
Finally, the techniques for proving these results
give us a way to obtain a large class of
examples that have small Resolution refutations but require
relatively large width. This answers a question of Alekhnovich
and Razborov \cite{AR01b} related to whether Resolution is
automatizable in quasipolynomial-time.