** Answer **

- a. (not p) < = > (q ^ r)
- b. p V q.
- c. p V w.
- d. w => r.
- e. p => (not (q ^ r))

** 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)

a(X) -- X is an adult.Express the following sentences in

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.

- 1. If B is a baby, then there exists an A who is taking care of B.

**Answer:**forall(B) b(B) => exists(A) c(A,B). - 2. If A is taking care of B, then for any place L, A is at L if and
only if B is at L.

**Answer:**forall(A,B,L) c(A,B) => [p(A,L) < = > p(B,L)]. - 3. If A is taking care of B, then A is an adult and B is a baby.

**Answer:**forall(A,B) c(A,B) => a(A) ^ b(B) - 4. If A is in the playground and A is an adult, then there exists a baby
B such that A is taking care of B. (That is, adults are only allowed in
the playground if they are taking care of a baby.)

**Answer:**forall(A,B) [p(A,g) ^ a(A)] => exists(B) b(B)^c(A,B). - 5. Everyone who is taking care of Joe is also taking care of Karen.

**Answer:**forall(X) c(X,j) => c(X,k). - 6. Joe and Karen are babies.

**Answer:**b(j) ^ b(k). - 7. If there are no babies in the playground, then there are no
adults in the playground.

**Answer:**[~exists(B) b(B) ^ p(B,g)] = > [~exists(A) a(A) ^ p(A,g)]. - 8. For every place L, if Joe is at L then Karen is at L.

**Answer:**forall(L) p(j,L) => p(k,L).

** Answer: **
The Skolemized forms of 1-6 are

(sk1(B) is a Skolem function mapping a baby B into some person taking care of B.)

(sk2 is a Skolem function mapping an adult A in the playground to a baby that A is taking care of.)

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

- 7a. ~b(B) V ~p(B,g).
- 7b. a(sk3).
- 7c. p(sk3,g)

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

- 8a. p(j,sk4).
- 8b. ~p(k,sk4).

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)