Logic - Proof of a resolution rule I am going to show the following resolution rule:
$$
(p \lor q) \land (\lnot p \lor r) \vdash (q \lor r)
$$
The proof I tried:
\begin{align}
&\quad \ (p \lor q) \land (\lnot p \lor r) \\
&\equiv ((p \lor q) \land \lnot p) \lor ((p \lor q) \land r) \\
&\equiv ((p \land \lnot p) \lor (\lnot p \land q)) \lor ((p \lor q) \land r) \\
&\equiv (\lnot p \land q) \lor ((p \lor q) \land r) \\
&\equiv ((\lnot p \land q) \lor(p \lor q)) \land ((\lnot p \land q) \lor r) \\
&\equiv (((\lnot p \land q) \lor p) \lor q) \land ((\lnot p \land q) \lor r) \\
&\equiv (((\lnot p \lor p) \land (p \lor q)) \lor q) \land ((\lnot p \land q) \lor r) \\
&\equiv (p \lor q) \land ((\lnot p \land q) \lor r) \\
&\equiv (p \lor q) \land (\lnot p \lor r) \land (q \lor r) \\
&\vdash (q \lor r)
\end{align}
It is strange that $(p \lor q) \land (\lnot p \lor r)$ appeared again with $q \lor r$ being connected by conjunction. Is this correct?
 A: Yes, it is correct ... you just derived the dual form of the Consensus Theorem:
$xy + x'z = xy + x'z + yz$
And if you look at a K-map, it's is actually not so strange, because it shows that the $YZ$ term is redundant given the other two.

A: Your sentenceial logic proof is valid.
$$\begin{array}{cll}
\quad & (p \lor q) \land (\lnot p \lor r) \\
\equiv& ((p \lor q) \land \lnot p) \lor ((p \lor q) \land r) &\text{distribution} \\
\equiv& (\lnot p \land q) \lor ((p \lor q) \land r) &\text{absorption} \\ 
\equiv& ((\lnot p \land q) \lor(p \lor q)) \land ((\lnot p \land q) \lor r) &\text{distribution} \\
\equiv& (((\lnot p \land q) \lor p) \lor q) \land ((\lnot p \land q) \lor r) &\text{association} \\
\equiv& ((p\lor q)\lor q)  \land ((\lnot p \land q) \lor r) &\text{absorption}\\
\equiv& (p \lor q) \land ((\lnot p \land q) \lor r) &\text{idemptoptence} \\
\equiv& (p \lor q) \land (\lnot p \lor r) \land (q \lor r) &\text{distribution} \\
\vdash& (q \lor r) &\text{simplification}
\end{array}
$$

It is strange that $(p \lor q) \land (\lnot p \lor r)$ appeared again with $q \lor r$ being connected by conjunction.

It is interesting, but not disturbing.  Since $q\lor r$ is entailed by $(p\lor q)\land(\lnot p\lor r)$, this is nothing more than a case of $$\begin{split}A~~\vdash&~ B\\\hline A\dashv\vdash&~ A\land B\end{split}$$
