Suppose a knowledge base contains just the following first-order Horn clauses: Ancestor(Mother(x), x) Ancestor (z. У) Л Ancestor (y, z) Ancestor (1,2) 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) (12) 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. (3) Ancestor(Mother(v), John)
ii. (3) Ancestor(Mother(Mother(y)), John)
iii. (3) Ancestor(Mother(Mother(Mother(v))), Mother())
iv. (8) Ancestor(Mother(Johm), Mother(Mother(John) ))
(b) (3) Can a resolution algorithm prove from the original knowledge base that -Ancestor(John, John)? Ex plain briefly
(c) (3) Suppose the KB is augmented with the assertion that -(Mother(x)-), and that the resolution algorithm includes inference rules for equality. Now what is the answer to (b)'?