Problem Set 4

Assigned: March 23
Due: April 6

Problem 1

Construct a resolution proof of sentence (F) from Problem set 3, Problem 3, sentences A-E. You should show (a) the Skolemized form of the axioms and of the negated goal; (b) each of the resolutions involved in the proof. You need not show the intermediate stages of the conversion to clausal form, or resolutions that a theorem prover might carry out but are not part of the final proof.

Note: The solutions to problem set 3 will be posted on or about March 30. You should check that you are starting from the right first-order encoding of the sentences.

Problem 2

Consider the following knowledge base:

1. parent(ed,anne).
2. parent(mary,anne)
3. parent(ed,bill)
4. parent(mary,bill)
5. parent(anne,george)
6. parent(bill,harry)
7. male(ed).
8. female(mary).
9. painter(mary).
10. soldier(george).

11. parent(X,Y) => child(Y,X).
12. child(X,Y) ^ male(X) => son(X,Y).
13. child(X,Y) ^ female(X) => daughter(X,Y).
14. parent(X,Y) => ancestor(X,Y)
15. parent(X,Y) ^ ancestor(Y,Z) => ancestor(X,Z).

What new facts can be inferred using forward chaining? (You should explain how facts are combined with the rules to get new facts; e.g.
Combining rule 11 with fact 1 under the substitution X=ed Y=anne gives the new fact
18. child(anne,ed).

Problem 3

Show how backward chaining can be used to prove the goals:
(A) son(Q,mary).
(B) ancestor(mary,R) ^ soldier(R).

You should trace paths that do not lead to a solution as well as those that do. Assume that backward chaining is executed in Prolog order. Your trace should follow the form in the backward chaining handout.