## Problem Set 4

Assigned: Oct. 4
Due: Oct 11.

### Problem 1

Trace the execution of the Davis-Putnam algorithm over the following set of clauses. When the algorithm must "guess" at a binding, it should choose the first unbound atom in alphabetical order, and should try TRUE before FALSE.
1. P V ~Q V R
2. P V R V X
3. ~P V ~R V W
4. ~P V Q V ~W
5. ~P V Q V W
6. ~Q V X
7. ~Q V ~X V Y
8. ~Q V ~Y

```
Initial set of clauses S0:

1. P V ~Q V R
2. P V R V X
3. ~P V ~R V W
4. ~P V Q V ~W
5. ~P V Q V W
6. ~Q V X
7. ~Q V ~X V Y
8. ~Q V ~Y

Initial valuation V0: All atoms unbound.

Call 1. dp1(ATOMS,S0,V0)
No singleton clauses, no pure literals
Try V[P]=TRUE.
Propagate: Delete clauses 1, 2, delete ~P from 3,4,5

Set S1:
3. ~R V W
4. Q V ~W
5. Q V W
6. ~Q V X
7. ~Q V ~X V Y
8. ~Q V ~Y
V1: V[P]=TRUE.

Call 2. dp1(ATOMS,S1,V1)
~R is a pure literal. Set V[R]=FALSE.  Delete 3.
4. Q V ~W
5. Q V W
6. ~Q V X
7. ~Q V ~X V Y
8. ~Q V ~Y
No singleton clauses, no pure literals.
Try V[Q]=TRUE.
Propagate: Delete 4, 5, delete ~Q from 6,7,8.

Set S2:
6. X
7. ~X V Y
8. ~Y
V2: V[P]=TRUE, V[Q]=TRUE, V[R]=FALSE.

Call 3. dp1(ATOMS,S2,V2)
6 is a singleton clause.  Set V[X]=TRUE. Delete 6, delete ~X from 7

7. Y
8. ~Y.

7 is a singleton clause. Set V[Y]=TRUE.  Delete 7, delete ~Y from 8.
8 is the empty clause. Fail call 3. Return to call 2.

In call 2: try V[Q]=FALSE. Delete 6,7,8. Delete Q from 4,5.
Set S3:
4. ~W.
5. W.
V3: V[P]=TRUE, V[Q]=FALSE, V[R]=FALSE.

Call 4. dp1(ATOMS,S3,V3)
4 is a singleton clause. Set V[W]=FALSE. Delete W from 5.
5 is the empty clause.  Fail call 4. Return to call 2

Fail call 2.
Try V[P] = FALSE. Propagate. Delete 3, 4, 5, delete P from 1, 2.
Set S5:
1. ~Q V R
2. R V X
6. ~Q V X
7. ~Q V ~X V Y
8. ~Q V ~Y
Valuation V5: V[P]=FALSE.

~Q is a pure literal. Set V[Q]=FALSE. Delete 1,6,7,8.

2. R V X

R is a pure literal. Set V[R]=TRUE.  Delete 2.
No clauses return. Succeed! Return valuation V[P]=TRUE, V[Q]=FALSE,
V[R]=TRUE.  V[W], V[X], and V[Y] may be assigned arbitrarily.
```

### Problem 2

Let U be a universe of people and classes. Let L be the first-order language with the following symbols:
m(P,Q) --- Person P has met person Q.
s(P,C) --- Person P is a student in class C.
t(P,C) --- Person P is the teacher of class C.
a,b --- Constants naming people Amy, and Barney .
d,e,f --- Constants naming classes Data Structures, English, French.
Express the following statements in L:
• A. Amy has not met the teacher of the English class.
Answer Either forall(P) t(P,e) => ~m(a,P)
or exists(P) t(P,e) ^ ~m(a,P)
is correct, as "the teacher of the English class" is presumably unique.
• B. There is a class in which all the students have met one another.
Answer exists(C) forall(P1,P2) s(P1,C) ^ s(P2,C) => m(P1,P2).
• C. There is a class in which some of the students have not met one another.
Answer exists(C,P1,P2) s(P1,C) ^ s(P2,C) ^ ~m(P1,P2).
• D. Everyone has met himself/herself (by definition).