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