We can do the same thing for resolution.

We already looked at that.

Resolution looks exactly like propositional resolution, except that we have to instantiate

with the most general unifier here.

And a little wrinkle here.

We need to be able to also collapse two variables by unification.

So instead of having one resolution rule, we have a resolution rule and a factorization

rule.

Let's make a real world example.

Say we have a law agent.

In real life you call those agents judges or attorneys or something like that.

And they know things.

The law says that it's a crime for an American to sell weapons to hostile nations.

The country NONO, an enemy of America, has some missiles and all of its missiles were

sold to it by Colonel West, who is in America.

Is there a problem here?

Well, yes.

We have to prove that Colonel West is a criminal and we're going to do it because he sold

weapons to hostile nations and hostile nations have something to do with being enemies of

America.

So that's the world and we're going to write this down in first world logic with the little

exception that instead of writing a clause like that, we kind of write it like this,

which makes it easier to read.

So it's a crime for an American to sell weapons to hostile nations.

If we know that X1 is an American and Y is a weapon and X1 sells Y1 to Z1 and Z1 is hostile,

then X1 is a crook or a criminal.

That's how nice it is to be able to write down things in first world logic.

You can almost directly kind of write it down.

NONO has some missiles.

There is an X that NONO owns and that is a missile and we directly make this into clauses.

We have no other variables so we can just instantiate a scolum function with no arguments

and then we have an AND here that makes two clauses.

We have a C that is owned by NONO and C is a missile.

All of NONO's missiles were sold by Colonel West.

So if X2 is a missile and it belongs to NONO, then West has sold it to NONO.

We know that missiles are weapons and an enemy of America is counted as hostile and West

is an American.

We also know that NONO is an enemy of America.

So there is a very good correspondence between this little text here and this first order

logic formula.

Actually, this first order logic formula in conjunctive normal form or clause normal form.

So we have written it down in first order logic.

We have made it into clauses and now we can start resolving.

Here is the resolution proof.

The important thing about this is this here.

It ends up in an empty clause.

Hooray.

All the other things are just resolution wranglings with these clauses.

And I'm going to look at a couple of them.

So we have a missile C and we have a clause, a missile Y, false, true and false, which