6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. 6.034 Notes: Section 10.1 Slide 10.1.1 A sentence written in conjunctive normal form looks like ((A or B or not C) and (B or D) and (not A) and (B or C)). Slide 10.1.2 Its outermost structure is a conjunction. It's a conjunction of multiple units. These units are called "clauses." Slide 10.1.3 A clause is the disjunction of many things. The units that make up a clause are called literals.6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. Slide 10.1.4 And a literal is either a variable or the negation of a variable. Slide 10.1.5 So you get an expression where the negations are pushed in as tightly as possible, then you have ors, then you have ands. This is like saying that every assignment has to meet each of a set of requirements. You can think of each clause as a requirement. So somehow, the first clause has to be satisfied, and it has different ways that it can be satisfied, and the second one has to be satisfied, and the third one has to be satisfied, and so on. Slide 10.1.6 You can take any sentence in propositional logic and write it in conjunctive normal form. Slide 10.1.7 Here's the procedure for converting sentences to conjunctive normal form.6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. Slide 10.1.8 The first step is to eliminate single and double arrows using their definitions. Slide 10.1.9 The next step is to drive in negation. We do it using DeMorgan's Laws. You might have seen them in a digital logic class. Not (phi or psi) is equivalent to (not phi and not psi). And, Not (phi and psi) is equivalent to (not phi or not psi). So if you have a negation on the outside, you can push it in and change the connective from and to or, or from or to and. Slide 10.1.10 The third step is to distribute or over and. That is, if we have (A or (B and C)) we can rewrite it as (A or B) and (A or C). You can prove to yourself, using the method of truth tables, that the distribution rule (and DeMorgan's laws) are valid. Slide 10.1.11 One problem with conjunctive normal form is that, although you can convert any sentence to conjunctive normal form, you might do it at the price of an exponential increase in the size of the expression. Because if you have A and B and C OR D and E and F, you end up making the cross-product of all of those things. For now, we'll think about satisfiability problems, which are generally fairly efficiently converted into CNF.6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. Slide 10.1.12 Here's an example of converting a sentence to CNF. Slide 10.1.13 First we get rid of both arrows, using the rule that says "A implies B" is equivalent to "not A or B". Slide 10.1.14 Then we drive in the negation using deMorgan's law. Slide 10.1.15 Finally, we distribute or over and to get the final CNF expression.6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. 6.034 Notes: Section 10.2 Slide 10.2.1 We have talked a little bit about proof, with the idea that you write down some axioms -- statements that you're given -- and then you try to derive something from them. And we've all had practice doing that in high school geometry and we've talked a little bit about natural deduction. So what we're going to talk about now is resolution. Which is the way that pretty much every modern automated theorem-prover is implemented. It seems to be the best way for computers to think about proving things. Slide 10.2.2 So here's the resolution inference rule, in the propositional case. It says that if you know "alpha or beta", and you know "not beta or gamma", then you're allowed to conclude "alpha or gamma". Remember from when we looked at inference rules before that these Greek letters are meta-variables. They can stand for big chunks of propositional logic, as long as the parts match up in the right way. So if you know something of the form "alpha or beta", and you also know that "not beta or gamma", then you can conclude "alpha or gamma". Slide 10.2.3 It turns out that this one rule is all you need to prove anything in propositional logic. At least, to prove that a set of sentences is not satisfiable. So, let's see how this is going to work. There's a proof strategy called resolution refutation, with three steps. It goes like this.6.034 Artificial Intelligence. Copyright © 2004 by Massachusetts Institute of Technology. Slide 10.2.4 First, you convert all of your sentences to conjunctive normal form. You already know how to do this! Then, you write each clause down as a premise or given in your proof. Slide 10.2.5 Then, you negate the desired conclusion -- so you have to say what you're trying to prove, but what we're going to do is essentially a proof by contradiction. You've all seen the strategy of proof by contradiction (or, if we're being fancy and Latin, reductio ad absurdum). You assert that the thing that you're trying to prove is false, and then you try to derive a contradiction. That's what we're going to do. So you negate the desired conclusion and convert that to CNF. And you add each of these clauses as a premise of your proof, as well. Slide 10.2.6 Now we apply the resolution rule until one of two things happens. We might derive "false", which means that the conclusion did, in fact, follow from the things that we had assumed. If you assert that the negation of the thing that you're interested in is true, and then you prove for a while and you manage to prove false, then you've succeeded in a proof by contradiction of the thing that you were trying to prove in the first place. Or, we might find ourselves in a situation where we can't apply the resolution rule any more, but we still haven't managed to derive false. Slide 10.2.7 What if you can't apply the resolution rule anymore? Is there anything in particular that you can conclude? In fact, you can conclude that the thing that you were trying to prove can't be proved. So resolution refutation for propositional logic is a complete proof procedure. If the thing that you're trying to prove is, in fact, entailed by the things that you've assumed, then you can prove it using resolution refutation. It's guaranteed that you'll always either prove false, or run out of possible steps. It's complete, because it always generates an answer. Furthermore, the process is sound: the
View Full Document
Unlocking...