<

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.

Answer:

Converting the sentences to clausal form gives the following. A.1. W(A,K).
A.2. W(A,G).
B. ~B(T,p1) V M(p1,SK1(p1)).
C.1. ~W(p1,s) V D(p1,s).
C.2. ~W(p1,s) V ~M(p1,p2) V D(p2,s).
D. B(T,A).
E. ~M(p1,p2) V ~W(p1,G) V ~W(p2,G).
Negation of F: W(p,G) V ~D(p,G).

Resolution proof:
Resolving B with D with binding p1=A gives
(G) M(A,SK1(A)).
Resolving C.2 with A.2 with binding p1=A, s=G gives
(H) ~M(A,p2) V D(p2,G).
Resolving H with G with binding p2=SK1(A) gives
(I) D(SK1(A),G).
Resolving G with E with binding p1=A, p2=SK1(A) gives <.br> (J) ~W(A,G) V ~W(SK1(A),G).
Resolving A.2 with J gives
(K) ~W(SK1(A),G).
Resolving F with I with binding p=SK1(A) gives
(L) W(SK1(A),G).
Resolving L with K gives the null clause.

Problem 2

Consider the following knowledge base:

Facts:
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).
10.A. male(bill).

Rules:
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).
Answer: Using the algorithm presented in class, in which one fact is resolved with one rule at each steps gives the following:

Combining rule 11 with fact 2 under the substitution X=mary, Y=anne gives the new fact
19. child(anne,mary).

Combining rule 11 with fact 3 under the substitution X=ed, Y=bill gives the new fact
20. child(bill,ed).

Combining rule 11 with fact 4 under the substitution X=mary, Y=bill gives the new fact
21. child(bill,mary).

Combining rule 11 with fact 5 under the substitution X=ed, Y=bill gives the new fact
22. child(george,anne).

Combining rule 11 with fact 5 under the substitution X=bill, Y=harry. gives the new fact
23. child(harry,bill).

Combining rule 12 with fact 18 under the substitution X=anne, Y=ed gives the new rule
24. male(anne) => son(anne,ed).

Combining rule 12 with fact 19 under the substitution X=anne, Y=mary gives the new rule
25. male(anne) => son(anne,mary).

Combining rule 12 with fact 20 under the substitution X=bill, Y=ed gives the new rule
26. male(bill) => son(bill,ed).

Combining rule 12 with fact 21 under the substitution X=bill, Y=mary gives the new rule
27. male(bill) => son(bill,mary).

Combining rule 12 with fact 22 under the substitution X=george, Y=anne gives the new rule
28. male(george) => son(george,anne).

Combining rule 12 with fact 23 under the substitution X=george, Y=anne gives the new rule
29. male(harry) => son(harry,bill).

Combining rule 13 with fact 18 under the substitution X=anne, Y=ed gives the new rule
30. female(anne) => daughter(anne,ed).

Combining rule 13 with fact 19 under the substitution X=anne, Y=mary gives the new rule
31. female(anne) => daughter(anne,mary).

Combining rule 13 with fact 20 under the substitution X=bill, Y=ed gives the new rule
32. female(bill) => daughter(bill,ed).

Combining rule 13 with fact 21 under the substitution X=bill, Y=mary gives the new rule
33. female(bill) => daughter(bill,mary).

Combining rule 13 with fact 22 under the substitution X=george, Y=anne gives the new rule
34. female(george) => daughter(george,anne).

Combining rule 13 with fact 23 under the substitution X=george, Y=anne gives the new rule
35. female(harry) => daughter(harry,bill).

Combining fact 1 with rule 14 under binding X=ed, Y=anne gives the new fact
36. ancestor(ed,anne)

Combining fact 2 with rule 14 under binding X=mary, Y=anne gives the new fact
37. ancestor(mary,anne)

Combining fact 3 with rule 14 under binding X=ed, Y=bill gives the new fact
38. ancestor(ed,bill)

Combining fact 4 with rule 14 under binding X=mary, Y=bill gives the new fact
39. ancestor(mary,bill)

Combining fact 5 with rule 14 under binding X=anne, Y=george gives the new fact
40. ancestor(anne,george).

Combining fact 6 with rule 14 under binding X=bill, Y=harry gives the new fact
41. ancestor(bill,harry).

Combining fact 1 with rule 15 under binding X=ed, Y=anne gives the new rule
42. ancestor(anne,Z) => ancestor(ed,Z).

Combining fact 2 with rule 15 under binding X=mary, Y=anne gives the new rule
43. ancestor(anne,Z) => ancestor(mary,Z).

Combining fact 3 with rule 15 under binding X=ed, Y=bill gives the new rule
44. ancestor(bill,Z) => ancestor(ed,Z).

Combining fact 4 with rule 15 under binding X=mary, Y=bill gives the new rule
45. ancestor(bill,Z) => ancestor(mary,Z).

Combining fact 5 with rule 15 under binding X=anne, Y=george gives the new rule
46. ancestor(george,Z) => ancestor(anne,Z).

Combining fact 6 with rule 14 under binding X=bill, Y=harry gives the new rule
47. ancestor(bill,Z) => ancestor(harry,Z).

Combining fact 10.A with rule 26 gives the new fact
48. son(bill,ed).

Combining fact 10.A with rule 27 gives the new fact
49. son(bill,mary).

Combining fact 40 with rule 42 under binding Z=george gives the new fact
50. ancestor(ed,george)

Combining fact 40 with rule 43 under binding Z=george gives the new fact
51. ancestor(mary,george)

Combining fact 41 with rule 44 under binding Z=harry gives the new fact
52. ancestor(ed,harry)

Combining fact 41 with rule 45 under binding Z=harry gives the new fact
53. ancestor(mary,harry)

The forward chaining algorithm described in the textbook (fig 9.3) uses a more efficient but more complicated algorithm, technically called "hyperresolution", in which one matches all the conditions on the left hand side against facts, and then infers the right-hand side. This cuts way down on the number of inferences that are made, but involves more complex matching. If this is used on the assignment, then inferences 24-35 and 42-47 go away, and inferences 48 to 53 have the following justifications:

Combining facts 20 and 10.A with rule 12 under the substitution X=bill, Y=ed gives
48. son(bill,ed)

Combining facts 21 and 10.A with rule 12 under the substitution X=bill, Y=ed gives
49. son(bill,mary)

Combining facts 1 and 40 with rule 15 under the substitution X=ed, Y=anne, Z=george gives
50. ancestor(ed,george).

Combining facts 2 and 40 with rule 15 under the substitution X=mary, Y=anne, Z=george gives
51. ancestor(mary,george).

Combining facts 3 and 41 with rule 15 under the substitution X=ed, Y=bill, Z=harry gives
52. ancestor(ed,harry).

Combining facts 4 and 41 with rule 15 under the substitution X=mary, Y=bill, Z=harry gives
53. ancestor(mary,harry).

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.

A:
G1: ?- son(Q,mary).                      Resolve with Rule 12
  G2:  ?- child(Q,mary), male(Q).        Resolve with rule 11
    G3:  ?- parent(mary,Q), male(Q)      Resolve with fact 2.
       G4:  ?- male(anne).               Fail.  Return to G3.
    G3:  ?- parent(mary,Q), male(Q)      Resolve with fact 4.
       G5: male(bill).                   Resolve with fact 10.A 
                                              Succeed with Q=bill
    G3:  Succeed with Q=bill
  G2:  Succeed with Q=bill
G1:  Succeed with Q=bill


B: 
G1: ?- ancestor(mary,R),soldier(R).            Resolve with rule 14
  G2:?- parent(mary,R),soldier(R).             Resolve with fact 2
   G3: ?- soldier(anne).                       Fail. return to G2.
  G2: ?- parent(mary,bill),soldier(R).         Resolve with fact 2
   G4: ?- soldier(bill).                       Fail. return to G2.
  G2: Fail. Return to G1
G1: ?- ancestor(mary,R),soldier(R).            Resolve with rule 15
  G5: ?- parent(mary,Y1),ancestor(Y1,R),soldier(R).  Resolve with fact 2
    G6:  ?- ancestor(anne,R), soldier(R).     Resolve with rule 14
      G7:  ?- parent(anne,R), soldier(R).     Resolve with fact 5. 
        G8: ?- soldier(george).               Resolve with fact 10. Succeed.
      G7: Succeed with R=george.
    G6: Succeed with R=george.
  G5: Succeed with R=george.
G1: Succeed with R=george.