Entailment in first-order logic using resolution 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?

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).