Logical resolution - Can we resolve two clauses without complementary literals? I am learning the resolution in propositional logic, and I understand that we can resolve two clauses like $\neg a \lor b$ and $\neg b \lor c$ to produce $\neg a \lor c$. But can we resolve $\neg a \lor b$ and $\neg c \lor d$? If we can, what is the result?
 A: No.  You can think about this intuitively.

*

*Either it is hot out or I am wearing a sweater.

*Either it is not hot out or I am wearing shorts.

From this, you can deduce

*

*Either I am wearing a sweater or I am wearing shorts.

But imagine there were four different propositions.

*

*Either it is hot out or I am wearing a sweater.

*Either it is not raining or I am carrying an umbrella.

Clearly, there is nothing we can do to combine and simplify these statements.
A: To reinforce the other given answer I thought it might be helpful to present a quick symbolic proof for the resolution rule (also equivalently known as hypothetical syllogism) so that you can see the importance of the shared term in the two disjunctions.

Given: $\neg a \vee b, \neg b \vee c$ 
Prove: $\neg a \vee c$
$(1) \ \ \neg a \vee b \ \ $ (premise) 
$(2) \ \ \neg b \vee c \ \ $ (premise) 
$(3) \ \ \textbf{Assume } a:$ 
$\ \ \ \ \ \ (4) \ \ b \ \ $ ($1, 3,$ disjunctive syllogism) 
$\ \ \ \ \ \ (5) \ \ c \ \ $ ($2, 4,$ disjunctive syllogism) 
$(6) \ \ \neg a \vee c \ \ $ (introducing an implication and cancelling the assumption at $3$)

So you can see between statements $(4)$ and $(5)$ the shared term provides a kind of bridge between the two statements. Without that shared term this argument is simply not possible.
