3
$\begingroup$

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$?

  • 0
    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.2012-04-14
  • 2
    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.2013-04-25

1 Answers 1