Are we allowed to resolve two variables at a time in CNF resolution?
For e.g. we have:
what will be the resolution of: $(P \lor \lnot Q \lor R) \land (\lnot P \lor Q \lor R)$
and what will be the resolution of: $(P \lor \lnot Q \lor R) \land (\lnot P \lor Q)$
Thanks, Hakid
No! Absolutely not!
Consider: You have $\{A, B \}$ and $\{\neg A, \neg B \}$
If you could resolve two at a time this would result in the empty clause $\{ \}$, which would suggest that the orginal clauses are not satisfiable. But clearly they are, e.g. set $A$ to True and $B$ to False.