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

Answer:

 
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. Return to call 1 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: