So, okay?

We are talking about first logic.

A geological logic, an expressive description language for almost everything.

Unless you want to do very specialized things, typically first or logic is a good description

language for it.

You can even do math with it with a couple of chin ups.

That goes beyond AI1.

We are in the middle of looking at machine oriented calculus for first logic.

Just a caveat before we even start, it is well known that first or logic is not decidable

anymore.

In propositional logic, we have decision procedures.

Have local calculus done right is terminating and thus gives us a program that you can

give any formula.

After a finite time, it stops and says yes, this is satisfiable or no, this is not satisfiable.

Yes, this is valid or no, this is not valid.

Or A is entailed from H1 to Hn.

All of those things we can decide in propositional logic.

In first or logic, which can talk about infinite domains, which is a good thing, more power,

can no longer be decided.

That is something to keep in mind.

We can't build an agent where we just say, oh, I want to know whether the Wumpus is in

3-1 and then just wait for the program to come back.

Because it might never.

We have no guarantee that our program will always reliably stop.

What we do have, however, at the theoretical side is we have semi-decision procedures.

A semi-decision procedure is an automated theorem, one of the things we are going to build.

We started looking at the calculus.

We don't have a unification yet, but otherwise we had the calculus yesterday.

Those are semi-decision procedures in the sense that if you are giving this theorem,

and you ask it, is this a theorem, is this valid?

If you give it a valid formula, it will stop at some point and say, yes, this is a theorem.

If you are giving it a normed theorem, there is no guarantee that it will stop.

It is slightly better than just knowing it is undecidable.

You kind of get half of the answers in finite time.

But if the procedure runs and runs and runs, you never quite know whether you have just

not waited long enough, and it is actually a theorem, or it is a non-theorem and it will

run forever.

Okay, so that is the logic we are talking about.

And we are using the tablo paradigm, which is a test calculus, which means instead of

going from the axioms to the theorems in a forward manner, we basically go backwards

from the negated theorems to the negated axioms.

And that is just better for machines.

And so we start with the negated formula, we go to the closures, which you can think of

as the negated axioms, or the simplest things that are inconsistent.

And if all the branches close, then we say, hooray, we have a proof.

What you are seeing here, or there is the calculus for propositional logic, and we have beefed

it up by new rules, the quantifier rules for first-order logic.

And we have done it wrong, because the left hand rule up here is infinitely branching.

If you think about what this is, right, I have given you a calculus.

Every calculus induces a search problem.