Given a Knowledge Base use resolution to prove ∃x¬B(x)

Question

¬B(x) ∨ C(x), ¬C(K) ∨ D(L), ¬C(M) ∨ E(N), ¬D(w) ∨ ¬E(y). Given this knowledge base, use resolution to prove ∃x¬B(x).

I am really stuck with this one.

Answer 1

OK, first negate the conclusion, so you get $\neg \exists x \neg B(x)$

Then put this in prenex form (i.e. move quantifiers in front), so you get $\forall x \neg \neg B(x)$

Put formula after quantifiers into CNF: $\forall x B(x)$

Distribute universal quantifier over conjuncts: $\forall x B(x)$ (only one conjunct, so no change).

Change variables to get unique variables: $\forall z B(z)$ (you already use x,w, and y in your knowledge base, so use something different)

Drop quantifier: $B(z)$

And add to knowledge base:

1. $\neg B(x) \lor C(x)$

2. $\neg C(K) \lor D(L)$

3. $\neg C(M) \lor E(N)$

4. $\neg D(w) \lor \neg E(y)$

5. $B(z)$

Now resolve using unification:

6. $C(x)$ 1,5 (x/z)

7. $D(L)$ 2,6 (K/x)

8. $E(N)$ 3,6 (M/x)

9. $\neg E(y)$ 4,7 (L/w)

10. $\bot$ 8,9 (N/y)

So: adding the negation of the conclusion to the knowledge base leads to a contradiction. So, the conclusion follows from the knowledge base.