# Resolution rule in propositional calculus

I was thinking about a reverse case of validity of resolution rule and had a question about it.

Basically, let me state resolution rule first.

Suppose $C_1$ and $C_2$ are clauses such that a literal $l$ belongs to $C_1$ and a complementary literal $l'$ belongs to $C_2$. Then the resolvant $C$ of $C_1$ and $C_2$ is $(C_1 \cup C_2) \setminus \{l, l'\}$

Now with this rule, we know that always $C_1 \models C$ and $C_2 \models C$.

But, is it always true that $C \models C_1$ and $C \models C_2$?

-

## migrated from stackoverflow.comApr 14 '12 at 13:29

This question came from our site for professional and enthusiast programmers.

C1 and C2 are disjunctions and so is C. So indeed, C1 |= C and C2 |= C but C |= C1 or C |= C2 are not necessarily true. – Alexander Serebrenik Apr 14 '12 at 13:13
That isn't correct. The point of the resolution rules is that from $C_1$ and $C_2$, $C$ may be inferred, but $C$ can't (necessarily) be inferred from $C_1$ or $C_2$ alone. – Joshua Taylor Apr 25 '13 at 1:44

Now with this rule, we know that always $C_1 \models C$ and $C_2 \models C$.
This isn't true. Let $C_1 = \{p,q\}$ and $C_2 = \{\lnot q, r\}$. Then $C = \{p, r \}$. It's not the case that $\{p,r\}$ must be true when $\{p,q\}$ is true. For instance, consider the truth assignment that makes $q$ true, and $p$ and $r$ false. Then $C_1$ is satisfied, but $C$ is not. Similarly, the truth assignment that makes $p$, $q$, and $r$ false satisfies $C_2$, but not $C$. However, any truth assignment that satisfies both $C_1$ and $C_2$ also satisfies $C$.
But, is it always true that $C \models C_1$ and $C \models C_2$?
No. For example, consider the truth assignment that makes $p$ and $q$ false, and $r$ true. This satisfies $C$, but not $C_1$. Similarly, the truth assignment that makes $p$ and $q$ true and $r$ false satisfies $C$, but not $C_2$. However, since every literal in $C$ is in either $C_1$ or $C_2$, any truth assignment that satisfies $C$ must satisfy at least one of $C_1$ and $C_2$.