Solution Set 2

Problem 1

What is the result of doing alpha-beta pruning in the game tree shown below?


Problem 2

Use propositional resolution to prove (a) from (b-e).

Answer: Let f be the negation of a. Skolemizing b-f gives the following:

b. p V q.
c. p V w.
d. ~w V r
e. ~p V ~q V ~r.
f.1: ~p V q
f.2: ~p V r
f.3: p V ~q V ~r.

The proof is then:

g. q.          (f.1 + b, factoring)
h. p V r.      (c + d).
i. r.          (f.2 + h, factoring)
j. p V ~r      (g + f.3)
k. p.          (j + i).
l. ~q V ~r     (k + e)
m. ~r          (l + g)
n. Empty       (m+i)

Problem 3

Let L be a first-order languge where the entities are people and places. L contains the following non-logical symbols:
a(X) -- X is an adult.
b(X) -- X is a baby.
c(X,Y) -- X is taking care of Y.
p(X,L) -- X is at place L.
j,k -- Constants. Joe and Karen.
g -- Constant. The playground.
Express the following sentences in L:

Problem 4

Construct resolution proofs of (7) and of (8) from (1-6) in problem 3.

Answer: The Skolemized forms of 1-6 are

  • 1. ~b(B) V c(sk1(B),B).
    (sk1(B) is a Skolem function mapping a baby B into some person taking care of B.)
  • 2a. ~c(A,B) V ~p(A,L) V p(B,L).
  • 2b. ~c(A,B) V ~p(B,L) V p(A,L).
  • 3a. ~c(A,B) V a(A).
  • 3b. ~c(A,B) V b(B).
  • 4a. ~p(A,g) V ~a(A) V b(sk2(A)).
  • 4b. ~p(A,g) V ~a(A) V c(A,sk2(A)).
    (sk2 is a Skolem function mapping an adult A in the playground to a baby that A is taking care of.)
  • 5. ~c(X,j) V c(X,k).
  • 6a. b(j).
  • 6b. b(k).

    The Skolemized form of the negation of (7) is the set of three clauses

    (The negation of (7) is the statement that there are no babies in the playground but there is an adult in the playground. The Skolem function sk3 is that hypothetical adult.)

    The resolution proof proceeds as follows:

    8.  ~a(sk3) V c(sk3,sk2(sk3)).  (7c + 4)
    9.  c(sk3,sk2(sk3)).            (7b + 8)
    10. b(sk2(sk3)).                (9 + 3b)
    11. ~p(sk2(sk3),g)              (10 + 7a)
    12. ~p(sk3,L) V p(sk2(sk3),L)   (9 + 2a)
    13. ~p(sk3,g).                  (12 + 11)
    14. Null                        (13 + 7c).

    The Skolemized form of the negation of (8) is the pair of clauses

    (The negation of 8 is the statement that Joe is some place where Karen is not. The Skolem constant sk4 represents that hypothetical place.)

    The resolution proof proceeds as follows:

    15. c(sk1(j),j).            (6a + 1)
    16. c(sk1(j),k).            (15 + 5)
    17. ~p(j,L) V p(sk1(j),L).  (15 + 2b)
    18. p(sk1(j),sk4).          (17 + 8a).
    19. ~p(sk1(j),L) V p(k,L)   (16 + 2a)
    20. p(k,sk4).               (19 + 18)
    21. null                    (20 + 8b)