LISP PROGRAMMING

1. dog(X) animal(X)

2. dog(fido)

3. animal(Y) die(Y)

Add the negation of what we wish to prove

4. die(fido)

Resolving 1 and 3 under {Y/X}

5. dog(Y) die(Y)

Resolving 2 and 5 under {fido/Y}

6. die(fido)

Resolving 4 and 6

CONTRADICTION!

Since we have produced a contradiction, it follows that die(fido) must be true.