Edit Question

Exercise 9.23

Suppose a knowledge base contains just the following first-order Horn clauses:

\(Ancestor(Mother(x),x)\) \(Ancestor(x,y) \land Ancestor(y,z) \implies Ancestor(x,z)\)

Consider a forward chaining algorithm that, on the $j$th iteration, terminates if the KB contains a sentence that unifies with the query, else adds to the KB every atomic sentence that can be inferred from the sentences already in the KB after iteration $j-1$.

  1. For each of the following queries, say whether the algorithm will (1) give an answer (if so, write down that answer); or (2) terminate with no answer; or (3) never terminate.

    1. $Ancestor(Mother(y),John)$

    2. $Ancestor(Mother(Mother(y)),John)$

    3. $Ancestor(Mother(Mother(Mother(y))),Mother(y))$

    4. $Ancestor(Mother(John),Mother(Mother(John)))$

  2. Can a resolution algorithm prove the sentence $\lnot Ancestor(John,John)$ from the original knowledge base? Explain how, or why not.

  3. Suppose we add the assertion that $\lnot(Mother(x)x)$ and augment the resolution algorithm with inference rules for equality. Now what is the answer to (b)?

Answer Improve This Solution
View Answer
Request Answer