Bob Chen emailed to ask "What is a resolution derivation? We couldn't find the term in the 'Handbook of proof theory' (there it only mentions resolution refutations)."


My answer:  A resolution derivation is the same as a resolution refutation, except not requiring the final clause to be the empty clause.   In particular, if there is a resolution refutation of a clause $C$ from  a set of clauses $\Gamma$, then $\Gamma \vDash C$ holds.   (We proved this fact in class as part of proving the soundness of resolution.)


Sam