Section 10.3 Notes

6.034 Notes: Section 10.3 Slide 10.3.1 We are going to use resolution refutation to do proofs in first-order logic. It's a fair amount trickier than in propositional logic, though, because now we have variables to contend with. Slide 10.3.2 Let's try to get some intuition through an example. Imagine you knew "for all x, P of x implies Q of x." And let's say you also knew P(A). What would you be able to conclude? Q(A), right? You ought to be able to conclude Q(A). Slide 10.3.3 This is actually Aristotle's original syllogism: From "All men are mortal" and "Socrates is a man", conclude "Socrates is a mortal". Slide 10.3.4 So, how can we justify this conclusion formally? Well, the first step would be to get rid of the implication. Slide 10.3.5 Next, we could substitute the constant A in for the variable x in the universally quantified sentence. By the semantics of universal quantification, that's allowed. A universally quantified statement has to be true of every object in the universe, including whatever object is denoted by the constant symbol A. And now, we can apply the propositional resolution rule. The hard part is figuring out how to instantiate the variables in the universal statements. In this problem, it was clear that A was the relevant individual. But it not necessarily clear at all how to do that automatically. Slide 10.3.6 Now, we have to do two jobs before we can see how to do first-order resolution. The first is to figure out how to convert from sentences with the whole rich structure of quantifiers into a form that lets us use resolution. We'll need to convert to clausal form, which is a kind of generalization of CNF to first-order logic. The second is to automatically determine which variables to substitute in for which other ones when we're performing first-order resolution. This process is called unification. We'll do clausal form next, then unification, and finally put it all together. Slide 10.3.7 Clausal form (which is also sometimes called "prenex normal form") is like CNF in its outer structure (a conjunction of disjunctions, or an "and" of "ors"). But it has no quantifiers. Here's an example conversion. Slide 10.3.8 We'll go through a step-by-step procedure for systematically converting any sentence in first-order logic into clausal form. Slide 10.3.9 The first step you guys know very well is to eliminate arrows. You already know how to do that. You convert an equivalence into two implications. And anywhere you see alpha right arrow beta, you just change it into not alpha or beta. Slide 10.3.10 The next thing you do is drive in negation. You already basically know how to do that. We have deMorgan's laws to deal with conjunction and disjunction, and we can eliminate double negations. As a kind of extension of deMorgan's laws, we also have that not (for all x, alpha) turns into exists x such that not alpha. And that not (exists x such that alpha) turns into for all x, not alpha. The reason these are extensions of deMorgan's laws, in a sense, is that a universal quantifier can be seen abstractly as a conjunction over all possible assignments of x, and an existential as a disjunction. Slide 10.3.11 The next step is to rename variables apart. The idea here is that every quantifier in your sentence should be over a different variable. So, if you had two different quantifications over x, you should rename one of them to use a different variable (which doesn't change the semantics at all). In this example, we have two quantifications involving the variable x. It's especially confusing in this case, because they're nested. The rules are like those for a programming language: a variable is captured by the nearest enclosing quantifier. So the x in Q(x,y) is really a different variable from the x in P(x). To make this distinction clear, and to automate the downstream processing into clausal form, we'll just rename each of the variables. Slide 10.3.12 Now, here's the step that many people find confusing. The name is already a good one. Step four is to skolemize, named after a logician called Thoralf Skolem. Imagine that you have a sentence that looks like: there exists an x such that P(x). The goal here is to somehow arrive at a representation that doesn't have any quantifiers in it. Now, if we only had one kind of quantifier in first-order logic, it would be easy because we could just mention variables and all the variables would be implicitly quantified by the kind of quantifier that we have. But because we have two quantifiers, if we dropped all the quantifiers off, there's a mess, because you don't know which kind of quantification is supposed to apply to which variable. Slide 10.3.13 The Skolem insight is that when you have an existential quantification like this, you're saying there is such a thing as a unicorn, let's say that P means "unicorn". There exists a thing such that it's a unicorn. You can just say, all right, well, if there is one, let's call it Fred. That's it. That's what Skolemization is. So instead of writing exists an x such that P(x), you say P(Fred). The trick is that it absolutely must be a new name. It can't be any other name of any other thing that you know about. If you're in the process of inferring things about John and Mary, then it's not good to say, oh, there's a unicorn and it's John -because that's adding some information to the picture. So to Skolemize, in the simple case, means to substitute a brand-new name for each existentially quantified variable. Slide 10.3.14 For example, if I have exists x, y such that R(x,y), then it's going to have to turn into R(Thing1, Thing2). Because we have two different variables here, they have to be given different names. Slide 10.3.15 But the names also have to persist so that if you have exists x such that P(x) and Q(x), then if you skolemize that expression you should get P(Fleep) and Q(Fleep). You make up a name and you put it in there, but every occurrence of this variable has to get mapped into that same unique name. Slide 10.3.16 If you have different quantifiers, then you need to use different names. Slide 10.3.17 All right. If that's all we had to do it wouldn't be too bad. But there's one more case. We can illustrate it by looking at two interpretations of "Everyone loves someone". In the first case, there is a single y that everyone loves. So we do ordinary skolemization and decide to call that person Englebert. Slide 10.3.18 In the second case, there is a different y, potentially, for each x. So, if we were just to substitute in a single constant name for y, we'd lose that information. We'd get the same result as above, which would be wrong. So, when you are skolemizing an existential variable, you have to look at the other quantifiers that contain the one you're skolemizing, and instead of substituting in a new constant, you substitute in a brand new function symbol, applied to any variables that are universally quantified in an outer scope. Slide 10.3.19 In this case, what that means is that you substitute in some function of x, for y. Let's call it Beloved(x). Now it's clear that the person who is loved by x depends on the particular x you're talking about. Slide 10.3.20 So, in this example, we see that the existential variable w is contained in the scope of two universally quantified variables, x, and z. So, we replace it with G(x,z), which allows it to depend on the choices of x and z. Note also, that I've been using silly names for Skolem constants and functions (like Englebert and Beloved). But you, or the computer, are only obliged to use new ones, so things like F123221 are completely appropriate, as well. Slide 10.3.21 Now we can drop the universal quantifiers because we just replaced all of the existential quantifiers with Skolem constants or functions. Now there's only one kind of quantifier left, so we can just drop them without losing information. Slide 10.3.22 And then we convert to clauses. This just means multiplying out the and's and the or's, because we already eliminated the arrows and pushed in the negations. We'll return a set of sets of literals. A literal, in this case, is a predicate applied to some terms, or the negation of a predicate applied to some terms. I'm using set notation here for clauses, just to emphasize that they aren't lists; that the order of the literals within a clause and the order of the clauses within a set of clauses, doesn't have any effect on its meaning. Slide 10.3.23 Finally, we can rename the variables in each clause. It's okay to do that because for all x, P(x) and Q (x) is equivalent to for all y, P(y) and for all z, P(z). In fact, you don't really need to do this step, because we're assuming that you're always going to rename the variables before you do a resolution step. Slide 10.3.24 So, let's do an example, starting with English sentences, writing them down in first-order logic, and converting them to clausal form. Later, we'll do a resolution proof using these clauses. Slide 10.3.25 John owns a dog. We can write that in first-order logic as there exists an x such that D(x) and O(J, x). So, we're letting D stand for "is a dog" and O stand for "owns" and J stand for John. Slide 10.3.26 To convert this to clausal form, we can start at step 4, Skolemization, because the previous three steps are unnecessary for this sentence. Since we just have an existential quantifier over x, without any enclosing universal quantifiers, we can simply pick a new name and substitute it in for x. Let's call x Fido. This will give us two clauses with no variables, and we're done. Slide 10.3.27 Anyone who owns a dog is a lover of animals. We can write that in FOL as For all x, if there exists a y such that D(y) and O(x,y), then L(x). We've added a new predicate symbol L to stand for "is a lover of animals". Slide 10.3.28 First, we get rid of the arrow. Note that the parentheses are such that the existential quantifier is part of the antecedent, but the universal quantifier is not. The answer would come out very differently if those parens weren't there; this is a place where it's easy to make mistakes. Slide 10.3.29 Next, we drive in the negations. We'll do it in two steps. I find that whenever I try to be clever and skip steps, I do something wrong. Slide 10.3.30 There's no skolemization to do, since there aren't any existential quantifiers. So, we can just drop the universal quantifiers, and we're left with a single clause. Slide 10.3.31 Lovers of animals do not kill animals. We can write that in FOL as For all x, L(x) implies that (for all y, A(y) implies not K(x,y)). We've added the predicate symbol A to stand for "is an animal" and the predicate symbol K to stand for x kills y. Slide 10.3.32 First, we get rid of the arrows, in two steps. Slide 10.3.33 Then we're left with only universal quantifiers, which we drop, yielding one clause. Slide 10.3.34 We just have three more easy ones. "Either Jack killed Tuna or curiosity killed Tuna." Everything here is a constant, so we get K(J,T) or K(C,T). Slide 10.3.35 "Tuna is a cat" just turns into C(T). Slide 10.3.36 And "All cats are animals" is not C(x) or A(x). I left out the steps here, but I'm sure you can fill them in. Okay. Next, we'll see how to match up literals that have variables in them, and move on to resolution.