Also did first order resolution, which is the same thing in green, right?

Take the propositional rule, add most general unifiers to it, and you're done.

Well, almost.

Turns out it's wrong.

You need this rule too, otherwise you're not going to make progress.

One fact, when Robinson invented unification together with this calculus, he forgot that

rule.

So he published a paper which turns out to be one of the most cited papers in computer

science of all times.

And when he submitted it, he had forgotten the rule.

The reviewer said, no, that's not correct.

I have a counter example.

Gave it back to Robinson, Alan Robinson.

And he fixed the problem relatively easily, and now that's what we have.

The reviewer, we also know who that was.

That was Sussman, whom we'll find again later today in planning.

You may know the book of Abelson and Sussman on algorithms, which is one of the standard,

standard, standard, standard things.

That's essentially what happened.

And we looked at a couple of examples.

We had Colonel West, the criminal, where we kind of translated everything into first order

logic including things like all.

An enemy is essentially if there is an enemy, then West is an American, da, da, da, da,

and we get a resolution proof.

This is the typical thing, a resolution theorem prover, which you would typically, resolution

theorem provers are kind of for first order logic, resolution is still the best, the best

calculus for machine oriented proving.

So almost all first order theorem provers use some form of resolution, and a good resolution

theorem prover would prove this in a couple of milliseconds.

Of course, there's two problems here.

One is if you have a natural language problem, how do you go from here to there?

That's an only partially solved problem.

And AI is still at work, or computational linguistics is still at work doing that.

The logic can do it, but the translation doesn't quite do it.

And even the statement of the logic can do it is wrong.

It can do this extremely efficiently.

If you actually translate all the American laws, which is kind of in paper that much

or more, into first order logic and give the theorem prover all of it, which is really

what a judge has to do, or the prosecutor, then there's another problem.

Then the theorem prover kind of drowns in clauses.

Then it starts doing things and makes many, many, many more clauses.

And if it didn't drown before, it drowns then and can't find anything.

That's the state of the art, essentially.