I understand from Watson that "Resolution is a proof technique that works on conjunctive normal form expressions by (1) selecting two clauses that contain conflicting terms, (2) combining the terms contained in those two clauses, and then (3) canceling the terms that conflict"
So for example $(\lnot A \lor B) \land ( \lnot B \lor C)$ resolves to $( \lnot A \lor C)$
But I want to see the break down of steps that shows why I can cancel out B with $ \lnot B$
If $B$ is true, then by disjunctive syllogism, $C$ must be true, so $\lnot A \lor C$ is true by addition. And if $B$ is false, by disjunctive syllogism, $\lnot A$ must be true, so $\lnot A \lor C$ is true, again by addition.
This means that, whether $A$ is true or not, $\lnot A \lor C$ is true.
In another way, we can convert $\lnot A \lor B$ into $A \Rightarrow B$. This means that the statement is just $(A \Rightarrow B) \land (B \Rightarrow C)$. Here, we can accomplish chaining of implications to get $A \Rightarrow C$, and rewriting back, we have $\lnot A \lor C$.