As before: feel free to discuss how to solve the problems with other students in the class, but do your own writeup.
1. For each of the following pair of complementary literals, give the most general unifier if it exists, or if none exists, explain why. See the definition MGU in the textbook, figure 9.1. We use the convention that variables are Capitalized (X,Y,Z) and constants are lowercase (a,b,c), which is like Prolog but the reverse of the convention in the textbook. Be care about the scope of variables: variables with the same name that appear in different clauses are not the same variable.
p(a,b,c) | ~p(X,Y,Z) |
p(a,b,X) | ~p(X,b,Y) |
q(Y,g(a,b)) | ~q(g(X,X),Y) |
older(father(Y),Y) | ~older(father(X),john) |
knows(father(Y),Y) | ~knows(X,X) |
2. In 1901, the philosopher Bertrand Russell set the world of mathematics on its ear by pointing out that earlier attempts to write down a logic for set theory were inconsistent. His proof was based based on the fact that these earlier attempts allowed you to define "the set of all sets that are not members of themselves". If your your logic can do that, then it must be inconsistent. In this exercise, you will show that even in first-order logic, if you assert that such a set exists, you can derive a contradiction. Note that this does not mean that first-order logic is inconsistent (indeed, it is provably consistent!), but just that those particular assertions are inconsistent.
We use a single constant term "s" and the binary predicate "member". We want to assert:
In logical form, this is:
Converting to clausal CNF form gives:
Write down a resolution proof of the empty clause. Note that your proof will involve resolving against the same clause more than once.
3. Write a Prolog program that finds a solution to the following puzzle. Optional: run your program to confrim that it works. You can download a good free version of Prolog from http://www.swi-prolog.org/. You can check your answer by Googling "zebra puzzle", but be warned that many versions of the puzzle on the net have slightly different clues and solutions.
The Mini Zebra Puzzle
Question: Who owns the zebra? More generally, for each house: who lives there, what pet does he have, and what does he drink?
Notes: In Prolog, the atom "X=Y" is true if X and Y unify. The atom "X\=Y" is true if X and Y do not unifiy. One way to solve the puzzle is write a clause that guesses at a solution, and then verifies that it is correct. Think carefully about the predicates you will use. For example, is it better to have a predicate such as "Zebra(H)", where H is a house, or a predicate such as "House1pet(P)", where P is a pet?
Following is the full version of the Zebra puzzle. You can solve it as well if you like, but are not required to do so!