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

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: