Resolution Refutation with Entailments?

Question

I have the following knowledge base:

[R1] AvBv¬C
[R2] ¬Dv¬B
[R3] AvC

And using resolution refutation must prove that D⊨A (That D entails A). How do I add this as a negated goal to the KB and prove through resolution refutation that it is true? (Resolving rules together until I get an empty clause). I have done resolution refutation with the basic logical operators but I don't know how to go about dealing with the entailment operator.

Answer 1

You have to prove that the premises and $D$ entail $A$.

Thus, you have to consider:

1) $A \lor B \lor ¬C$

2) $¬D \lor ¬B$

3) $A \lor C$

4) $D$

and the negation of the conclusion: $\lnot A$.

Then, apply Resolution.

---

Alternatively, you can consider $D \to A$ as the sought conclusion; in this case, you have to add its negation to the premises, i.e. $\lnot(\lnot D \lor A) \equiv (D \land \lnot A)$.

And the result is the same: you have to add to the three initial clauses the two formulas: $D$ and $\lnot A$.