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 ...
more >>>