The resources I've come across mention that

When the two clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair; however, the result is always a tautology, and thus discarded.

As I understand it, this statement means

$A \vee B, \quad A \vee \neg B \Rightarrow A$ is the right resolution


$A \vee B \vee \neg C, \quad A \vee \neg B \vee C \Rightarrow A$ is not

However I don't really get what it means. I think I understand what is a tautology, however how does the result of such a resolution step become a tautology, and why do we have to discard it instead of adding it to the set of clauses? More detailed explanation isn't provided in the resources I've found.


If you have $$ A \lor B \lor \neg C \quad\text{and}\quad A \lor \neg B \lor C $$ you can apply resolution to either $(\neg)B$, producing $$ A \lor \neg C \lor A \lor C $$ or to $(\neg)C$, producing $$ A \lor B \lor A \lor \neg B $$ Both of these results are tautologies, however, so they are useless -- knowing that they are true does not tell us anything about the possible truth values of $A$, $B$, and $C$.

But you cannot apply resolution to both $(\neg)B$ and $(\neg)C$ at the same time and get $A\lor A$ -- that's just not how the resolution rule works. (And for good reason; this very example shows that it would be unsound to do so. If all three variables are false, then the two original clauses are both true but $A\lor A$ is false, so you would have concluded something false starting with truth).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.