Sections 9.3-9.4 Notes

6.034 Notes: Section 9.3 Slide 9.3.1 One reason for writing down logical descriptions of situations is that they will allow us to draw conclusions about other aspects of the situation we've described. Slide 9.3.2 Imagine that we knew the following things to be true: If today is sunny, Tomas will be happy; if Tomas is happy, the lecture will be good; and today is sunny. Does this mean that the lecture will be good? Slide 9.3.3 One way to think about this is to start by figuring out what set of interpretations make our original sentences true. Then, if G is true in all those interpretations, it must be okay to conclude it from the sentences we started out with (sometimes called our knowledge base). Slide 9.3.4 In a universe with only three variables, there are 8 possible interpretations in total. Slide 9.3.5 Only one of these interpretations makes all the sentences in our knowledge base true: S = true, H = true, G = true. Slide 9.3.6 And it's easy enough to check that G is true in that interpretation, so it seems like it must be reasonable to draw the conclusion that the lecture will be good. (Good thing!). Slide 9.3.7 If we added another variable to our domain, say whether Leslie is happy (L), then we'd have two interpretations that satisfy the KB: S = true, H = true, G = true, L = true; and S = true, H = true, G = true, L = false. G is true in both of these interpretations, so, again, if the KB is true, then G must also be true. Slide 9.3.8 There is a general idea called "entailment" that signifies a relationship between a knowledge base and another sentence. If whenever the KB is true, the conclusion has to be true (that is, if every interpretation that satisfies the KB also satisfies the conclusion), we'll say that the KB "entails" the conclusion. You can think of entailment as something like "follows from", or "it's okay to conclude from". Slide 9.3.9 The method of enumerating all the interpretations that satisfy the KB, and then checking to see if the conclusion is true in all of them is a correct way to test entailment. Slide 9.3.10 But now, what if we were to add 6 more propositional variables to our domain? Then we'd have 2^10 = 1024 interpretations to check, which is way too much work to do (and, in the first order case, we'll find that we might have infinitely many intepretations, which is definitely too much work to enumerate!!). Slide 9.3.11 So what we'd really like is a way to figure out whether a KB entails a conclusion without enumerating all of the possible interpretations. A proof is a way to test whether a KB entails a sentence, without enumerating all possible interpretations. You can think of it as a kind of shortcut arrow that works directly with the syntactic representations of the KB and the conclusion, without going into the semantic world of interpretations. Slide 9.3.12 So what is a proof system? Well, presumably all of you have studied high-school geometry; that's often people's only exposure to formal proof. Remember that? You knew some things about the sides and angles of two triangles and then you applied the side-angle-side theorem to conclude -- at least people in American high schools were familiar with side-angle-side -- The side-angle-side theorem allowed you to conclude that the two triangles were similar, right? That is formal proof. You've got some set of rules that you can apply. You've got some things written down on your page, and you grind through, applying the rules that you have to the things that are written down, to write some more stuff down until finally you've written down the things that you wanted to, and then you get to declare victory. That's a proof. There are (at least) two styles of proof system; we're going to talk about one briefly here and then go on to the other one at some length in the next two sections. Natural deduction refers to a set of proof systems that are very similar to the kind of system you used in high-school geometry. We'll talk a little bit about natural deduction just to give you a flavor of how it goes in propositional logic, but it's going to turn out that it's not very good as a general strategy for computers. It's a proof system that humans like, and then we'll talk about a proof system that computers like, to the extent that computers can like anything. Slide 9.3.13 A proof is a sequence of sentences. This is going to be true in almost all proof systems. Slide 9.3.14 First we'll list the premises. These are the sentences in your knowledge base. The things that you know to start out with. You're allowed to write those down on your page. Sometimes they're called the "givens." You can put the givens down. Slide 9.3.15 Then, you can write down on a new line of your proof the results of applying an inference rule to the previous lines. Slide 9.3.16 Then, when a sentence S is on some line, you have proved S from KB. Slide 9.3.17 If your inference rules are sound, then any S you can prove from KB is, in fact, entailed by KB. That is, it's legitimate to draw the conclusion S from the assumptions in KB. Slide 9.3.18 If your rules are complete, then you can use KB to prove any S that is entailed by the KB. That is, you can prove any legitimate conclusion. Wouldn't it be great if you were sound and complete derivers of answers to problems? You'd always get an answer and it would always be right! Slide 9.3.19 So let's look at inference rules, and learn how they work by example. We'll look at natural-deduction rules first, because they're easiest to understand. Slide 9.3.20 Here's a famous one (first written down by Aristotle); it has the great Latin name, "modus ponens", which means "affirming method". It says that if you have "Alpha implies Beta" written down somewhere on your page, and you have Alpha written down somewhere on your page, then you can write beta down on a new line. (Alpha and Beta here are metavariables, like Phi and Psi, ranging over whole complicated sentences). It's important to remember that inference rules are just about ink on paper, or bits on your computer screen. They're not about anything in the world. Proof is just about writing stuff on a page, just syntax. But if you're careful in your proof rules and they're all sound, then at the end when you have some bit of syntax written down on your page, you can go back via the interpretation to some semantics. So you start out by writing down some facts about the world formally as your knowledge base. You do stuff with ink and paper for a while and now you have some other symbols written down on your page. You can go look them up in the world and say, "Oh, I see. That's what they mean." Slide 9.3.21 Here's another inference rule. "Modus tollens" (denying method) says that, from "alpha implies beta" and "not beta" you can conclude "not alpha". Slide 9.3.22 And-introduction say that from "Alpha" and from "Beta" you can conclude "Alpha and Beta". That seems pretty obvious. Slide 9.3.23 Conversely, and-elimination says that from "Alpha and Beta" you can conclude "Alpha". Slide 9.3.24 Now let's do a sample proof just to get the idea of how it works. Pretend you're back in high school Slide 9.3.25 We'll start with 3 sentences in our knowledge base, and we'll write them on the first three lines of our proof: (P and Q), (P implies R), and (Q and R imply S). Slide 9.3.26 From line 1, using the and-elimination rule, we can conclude P, and write it down on line 4 (together with a reminder of how we derived it). Slide 9.3.27 From lines 4 and 2, using modus ponens, we can conclude R. Slide 9.3.28 From line 1, we can use and-elimination to get Q. Slide 9.3.29 From lines 5 and 6, we can use and-introduction to get (Q and R). Slide 9.3.30 Finally, from lines 7 and 3, we can use modus ponens to get S. Whew! We did it! Slide 9.3.31 The process of formal proof seems pretty mechanical. So why can't computers do it? They can. For natural deduction systems, there are a lot of "proof checkers", in which you tell the system what conclusion it should try to draw from what premises. They're always sound, but nowhere near complete. You typically have to ask them to do the proof in baby steps, if you're trying to prove anything at all interesting. Slide 9.3.32 Part of the problem is that they have a lot of inference rules, which introduces a very big branching factor in the search for proofs. Slide 9.3.33 Another big problem is the need to do "proof by cases". What if you wanted to prove R from (P or Q), (Q implies R), and (P implies R)? You have to do it by first assuming that P is true and proving R, then assuming Q is true and proving R. And then finally applying a rule that allows you to conclude that R follows no matter what. This kind of proof by cases introduces another large amount of branching in the space. Slide 9.3.34 An alternative is resolution, a single inference rule that is sound and complete, all by itself. It's not very intuitive for humans to use, but it's great for computers. Resolution requires all sentences to be first written in a special form. So the next section will investigate that special form, and then we'll return to resolution. 6.034 Notes: Section 9.4 Slide 9.4.1 Now we're going to start talking about first-order logic, which extends propositional logic so that we can talk about things. Slide 9.4.2 In propositional logic, all we had were variables that stood, not for things in the world or even quantities, but just facts, Boolean statements that might or might not be true about the world, like whether it's raining, or greater than 67 degrees; but you couldn't have variables that stood for tables or books, or the temperature, or anything like that. And as it turns out, that's an enormously limiting kind of representation. Slide 9.4.3 In first-order logic, variables refer to things in the world and you can quantify over them. That is, you can talk about all or some of them without having to name them explicitly. Slide 9.4.4 There are lots of examples that show how propositional logic is inadequate to characterize even moderately complex domains. Here are some more examples of the kinds of things that you can say in first-order logic, but not in propositional logic. Slide 9.4.5 "When you paint the block, it becomes green." You might have a proposition for every single aspect of the situation, like "if this block is black and I paint it, it becomes green" and "if that block is red and I paint it, it becomes green" and "if block #5 is green and I paint it, it becomes green". But you'd have to have one of those propositions for every single initial block color, or every single block, or every single object (if you have non-blocks, too) in the world. You couldn't say that, as a general fact, "after you paint something if becomes green." Slide 9.4.6 Let's say you want to talk about what happens when you sterilize a jar. It kills all the bacteria in the jar. Now, you don't want to have to name all the bacteria; to have to say, bacterium 57 is dead, and bacterium 93 is dead. Each one of those guys is dead. All the bacteria are dead now. So you'd like to have a way not only to talk about things in the world, but to talk about all of them, or some of them, without naming any of them explicitly. Slide 9.4.7 In the context of providing flexible computer security, you might want to prove or try to understand whether someone should be allowed access to a web site. And you could say: a person should have access to this web site if they've been personally, formally authorized to use this web site or if they are known to someone who has access to the web site. So you could write a general rule that says that and then some other system or this system could try to prove that you should have access to the web site. In this case, what that would mean would be going to look for a chain of people that are authorized or known to one another that bottoms out in somebody who's known to this web site. Slide 9.4.8 First-order logic lets us talk about things in the world. It's a logic like propositional logic, but somewhat richer and more complex. We'll go through the material in the same way that we did propositional logic: we'll start with syntax and semantics, and then do some practice with writing down statements in first-order logic. Slide 9.4.9 The big difference between propositional logic and first-order logic is that we can talk about things, and so there's a new kind of syntactic element called a term. And the term, as we'll see when we do the semantics, is a name for a thing. It's an expression that somehow names a thing in the world. There are three kinds of terms: Slide 9.4.10 There are constant symbols. They are names like Fred or Japan or Bacterium39. Those are symbols that, in the context of an interpretation, name a particular thing. Slide 9.4.11 Then there are variables, which are not really syntactically differentiated from constant symbols. We'll use capital letters to start constant symbols (think of them as proper names), and lower-case letters for term variables. (It's important to note, though, that this convention is not standard, and in some logic contexts, such as the programming language Prolog, they adopt the exact opposite convention). Slide 9.4.12 The last kind of term is a function symbol, applied to one or more terms. We'll use lower-case for function symbols as well. So another way to make a name for something is to say something like f(x). If f is a function, you can give it a term and then f(x) names something. So, you might have mother-of (John) or f(f(x)). Note that a function with no terms would be a constant. These three kinds of terms are our ways to name things in the world. Slide 9.4.13 In propositional logic we had sentences. Now, in first-order logic it's a little bit more complicated, but not a lot. So what's a sentence? There's another kind of symbol called a predicate symbol. A predicate symbol is applied to zero or more terms. Predicate symbols stand for relations, so we might have things like On(A,B) or Sister(Jane, Joan). On and Sister are predicate symbols; a, b, Jane, Joan, and mother-of(John) are terms. A predicate applied to zero terms is what's sometimes called a sentential variable or a propositional variable. It was our old kind of variable that we had before in propositional logic, like "it's-raining." It's a little bit of an artifice, but we'll take predicates with no arguments to be variables that have values true or false. Slide 9.4.14 A sentence can also be of the form t1 = t2. We're going to have one special predicate called equality. You can say this thing equals that thing, written term, equal-sign, term. Slide 9.4.15 There are two more new constructs. If v is a variable and Phi is a sentence then (upside-down-A v . phi), and (backwards-E v . phi) are sentences. You've probably seen these symbols before informally as "for all" and "there exists", and that's what they're going to mean for us, too. Slide 9.4.16 Finally we have closure under the sentential operators that we had before, so you can make complex sentences out of other sentences using and, or, not, implies, equivalence (also called biconditional), and parentheses, just as before in propositional logic. All that basic connective structure is still the same, but the things that we can say on either side have gotten a little bit more complicated. All right, that's our syntax. That's what we get to write down on our page.