Entailment in first-order logic using resolution

Question

I have the following sentences in the KB:

1) (¬Y(x) v F(x)) ^ (¬Y(x) v D(x) v C(x))
2) Y(something)
3) ¬C(x) v L(x)
4) ¬D(x) v L(x)

And am trying to find if the sentence L(something) is entailed. So we would add another sentence to the KB

5) ¬L(something)

Because only sentence 1 has F(x), there would be no way to reach a contradiction using it. Thus, we would be left with the last 4 sentences to use, which just by looking them, looks like there would be no way to reach a contradiction. Thus, it would seem the KB does not entail L(something).

I'd like to know if my line of thinking is correct. If it is, how would I formally show there is no entailment of L(Something)? Or if not, where in my logic am I going wrong?

Answer 1

First: list all the clauses:

1) $¬Y(x) \lor F(x)$

2) $¬Y(x) \lor D(x) \lor C(x)$

3) $Y(s)$ --- $s$ for something

4) $¬C(x) \lor L(x)$

5) $¬D(x) \lor L(x)$

Second: add the negation of the sought conclusion:

6) $\lnot L(s)$.

Third: replace $x$ with $s$.

Fourth : apply Resolution:

7) $L(s) \lor ¬Y(s) \lor D(s)$ --- from 2) and 4)

8) $L(s) \lor ¬Y(s)$ --- from 5) and 7)

9) $L(s)$ --- from 3) and 8)

10) $\square$ --- the empty clause: from 6) and 9).