Notes on Lectures
When solving 9.9 (Problem 2 of Assignment 5), you might find it easier to tackle g before f. Suppose we want to (as in g) show that B follows from A. (You should already know whether or not this will work, given your answer to previous parts of 9.9) To prove that KB |= a, you use resolution to show that KB V ¬a is unsatisfiable. Think about that for a moment -- why is that? (Answer) Start by picking one statement to be the KB and the second to be the statement whose entailment you are interested in. Then add the negation of the statement to the KB (remember we're trying to show that KB V ¬a is unsatisfiable). Next, we try to derive a contradiction, because that's how we show unsatisfiability. To translate the sentences into canoncial form, see the section entitled Conversion to Normal Form in Section 9.6 in the text.
You need to do two things in this case: get rid of the negation in ¬a, and dump the quantifiers. Getting rid of universal quantifiers is easy because we'll just assume that all variables are unviersally quantified. To get rid of existential quantifiers is a bit more work, because you need to Skolemize the statements (A and B). This is a little awkward, but the bottom of page 281 and top of 282 show what you need to do.Once you've introduced the Skolem functions, you proceed as you normally would. In other words the Skolem functions (lets call them F1(x) and F2(y) can be bound to variables, such as x and y. However, there is one danger in the unification that we haven't discussed yet. What happens if a variable is bound to an expression that contains itself? Should we allow that to happen, and if not, what do we do when the only binding has this circularity property?
Closures are covered in Chapter 6 of the Lisp book, in section 6.5. You should be familiar with closures (i.e. how to create them and why they're useful). Be sure that you understand the distinction between dynamic scope and lexical scope, and how dynamically scoped variables interact with closures.
The missionaries and cannibals problem is described in Chapter 3, and includes a description of the states, operators and all the other fun details.
The only way for the disjunction to be FALSE is for both terms to be FALSE, so that would mean that ¬a would be FALSE. Thus, either a is TRUE or KB is FALSE. Writing the last statement in logical form gives a V ¬KB, but that's just another way of writing KB => a. (Return to resolution)