1Lecture 7 • 1 6.825 Techniques in Artificial Intelligence Resolution Theorem Proving: Propositional Logic • Propositional resolution • Propositional theorem proving •Unification Today we’re going to talk about resolution, which is a proof strategy. First, we’ll look at it in the propositional case, then in the first-order case. It will actually take two lectures to get all the way through this. Then, we’ll have you do problem set 2, which involves using the resolution proof technique on a moderately big problem in first-order inference.2Lecture 7 • 2 Propositional Resolution At the end of propositional logic, we talked a little bit about proof, what it was, 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 today is resolution. Which is the way that pretty much every modern automated theorem-prover is implemented. It's apparently the best way for computers to think about proving things.3Lecture 7 • 3 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ 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”. OK. 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”.4Lecture 7 • 4 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ • Resolution refutation: It turns out that that one rule is all you need to prove things. 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. And it goes like this.5Lecture 7 • 5 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ • Resolution refutation: • Convert all sentences to CNF 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.6Lecture 7 • 6 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ • Resolution refutation: • Convert all sentences to CNF • Negate the desired conclusion (converted to CNF) 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.7Lecture 7 • 7 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ • Resolution refutation: • Convert all sentences to CNF • Negate the desired conclusion (converted to CNF) • Apply resolution rule until either – Derive false (a contradiction) – Can’t apply any more And then we apply the Resolution Rule until either you can derive "false" -- which means that the conclusion did, in fact, follow from the things that you had assumed, right? 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. So you run the resolution rule until you derive false or until you can't apply it anymore.8Lecture 7 • 8 Propositional Resolution • Resolution rule: α v β ¬β v γ α v γ • Resolution refutation: • Convert all sentences to CNF • Negate the desired conclusion (converted to CNF) • Apply resolution rule until either – Derive false (a contradiction) – Can’t apply any more • Resolution refutation is sound and complete • If we derive a contradiction, then the conclusion follows from the axioms • If we can’t apply any more, then the conclusion cannot be proved from the axioms. 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. So 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. In the propositional case. It’s more complicated in the first-order case, as we’ll see. But in the propositional case, it means that if you've applied the Resolution Rule and you can't apply it anymore, then your desired conclusion can’t be proved. 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 answer is always correct.9Lecture 7 • 9 Propositional Resolution Example DerivationFormulaStep Q → R3 P → R2 P v Q1 Prove R So let's just do a proof. Let's say I'm given “P or Q”, “P implies R” and “Q implies R”. I would like to conclude R from these three axioms. I'll use the word "axiom" just to mean things that are given to me right at the moment.10Lecture 7 • 10 Propositional Resolution Example DerivationFormulaStep GivenP v Q1 Q → R3 P → R2 P v Q1 Prove R We start by converting this first sentence into conjunctive normal form. We don’t actually have to do anything. It’s already in the right form.11Lecture 7 • 11 Propositional Resolution Example DerivationFormulaStep Given ¬ P v R2 GivenP v Q1 Q → R3 P → R2 P v Q1 Prove R Now, “P implies R” turns into “not P or R”.12Lecture 7 • 12 Propositional Resolution Example DerivationFormulaStep Given ¬ Q v R3 Given ¬ P v R2 GivenP v Q1 Q → R3 P → R2 P v Q1 Prove R Similarly, “Q implies R” turns into “not Q or R13Lecture 7