## AI: Problem Set 3

Assigned: Feb. 19
Due: March 2

### Problem 1

Let D be the domain of solid objects. Let L be the first-order language over D with the following non-logical symbols:
inside(O1,O2) --- Object O is inside O2.
empty(O) --- Object O is empty.
accessible(O) --- Object O is accessible.
red(O) --- Object O is red.
Represent the following statements in L.
• A. An object is empty if and only if there is nothing inside it.
forall(O1) empty(O1) < = > ~ exists(O2) inside(O2,O1).
• B. An object is accessible if and only if it is not inside any object.
forall(O1) accessible(O1) < = > ~ exists(O2) inside(O1,O2).
• C. Every object is either accessible or inside some accessible object.
forall(O) accessible(O) V exists(O2) accessible(O2) ^ inside(O,O2).
• D. All the accessible objects are red.
forall(O) accessible(O) => red(O).
• E. If O1 is inside O2 and O2 is red, then O1 is red.
forall(O1,O2) inside(O1,O2) ^ red(O2) => red(O1).
• F. If all objects are accessible, then all objects are empty.
[forall(O) accessible(O)] => [forall(O) empty(O)]
• G. All objects are red.
forall(O) red(O).

### Problem 2

Convert sentences A through E above, and the negations of sentences F and G to clausal form (CNF).
• A.1. ~empty(O1) V ~inside(O2,O1).
• A.2. empty(O1) V inside(sk1(O1),O1).
• B.1. ~accessible(O1) V ~inside(O1,O2)
• B.2. accessible(O1) V inside(O1,sk2(O1)).
• C.1. accessible(O) V accessible(sk3(O)).
• C.2. accessible(O) V inside(O,sk3(O)).
• D. ~accessible(O) V red(O).
• E. ~inside(O1,O2) V ~red(O2) V red(O1).
• [not F].1. accessible(O).
• [not F].2. ~empty(sk4)
• [not G]~red(sk5).

### Problem 3

Give resolution proofs of F and G from A-E. (No credit will be given for a proof that is not a resolution proof.)

#### Proof of F

```H. inside(sk1(sk4),sk4).  From [not F].2 and A.2, O1 -> sk4.
I. ~accessible(sk1(sk4)). From H and B.1, O1 -> sk1(sk4), O2 -> sk4
J. empty clause.          From I and [not F].1, O -> sk1(sk4).
```

#### Proof of G

```K. ~accessible(sk5).      From [not G] and D. O -> sk5
L. accessible(sk3(sk5)).  From K and C.1. O -> sk5.
M. inside(sk5,sk3(sk5)).  From K and C.2, O -> sk5.
N. red(sk3(sk5)).         From L and D.   O -> sk3(sk5).
P. ~red(sk3(sk5)) V red(sk5). From M and E, O1 -> sk5, O2 -> sk3(sk5).
Q. red(sk5).              From P and N.
R. empty                  From Q and [not G].
```