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

Ancestor(Mother(x), x)

Ancestor(x, y) ∧ Ancestor(y, z) ⇒ Ancestor(x, z)

Consider a forward chaining algorithm that, on the jth 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.

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

(i) Ancestor(Mother(y), John)

(ii) Ancestor(Mother(Mother(y)), John)

(iii) Ancestor(Mother(Mother(Mother(y))),Mother(y))

(iv) Ancestor(Mother(John),Mother(Mother(John)))

b. Can a resolution algorithm prove the sentence ¬Ancestor(John,John) from the original knowledge base? Explain how, or why not.

c. Suppose we add the assertion that ¬(Mother(x)=x) and augment the resolution algorithm with inference rules for equality. Now what is the answer to (b)?