Using resolution in first order logic to prove a pink elephant likes a gray elephant

Question

Given the following logical theory:

$$ 1 \space Pink(Sam) $$

$$ 2 \space Gray(Clyde) $$

$$ 3 \space Likes(Clyde,Oscar) $$

$$ 4 \space Likes(Oscar,Sam) $$ $$ 5 \space \neg (Pink(Oscar) \land Gray(Oscar)) $$

$$ 6 \space \neg ( \neg Pink(Oscar) \land \neg Gray(Oscar)) $$

Use resolution to show that a pink elephant likes a gray elephant by answering the following questions.

a) Convert the formulas 1 to 6 into CNF.

Doing so yields me the same for each one of them except for the last two. Using De morgans law I end up with:

$$ 5 \space (\neg Pink(Oscar) \lor \neg Gray(Oscar)) $$

And $$ 6 \space ( Pink(Oscar) \lor Gray(Oscar)) $$

This is where it gets tricky for me. I can see that in my KB, 5 and 6 are each others inverse, so if I would use resolution between the two I would end up with the empty clause directly. How would I go about to solve this exercise?

b) Prove that $$ \exists x\exists y (Gray(x) \land Pink(y) \land Likes(x,y)) $$

Is a logical consequence of (1) - (6) Using the resolution proof technique

Answer 1

Steps 5 and 6 are fine, but then you get e.g.

$Gray(Oscar)∨¬Gray(Oscar)$.

The Resolution procedure says :

"The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology)."

$p∨¬p$ is not the empty clause : $\square$ or $\bot$. The empty clause is always false while a tautology is always true.

"Physically" the empty clause is $\{ \quad \}$ i.e. a clause with no formula inside. This is different form e.g. $\{ p∨¬p \}$.