Okay, welcome back.

We are talking about inference procedures that are amenable for implementation, because

after all we want to build agents, at least in principle.

And yesterday we've talked about two kinds of inference procedures, machine oriented

inference procedures.

The first one was tableau and the second one was resolution.

Today, yeah and the idea behind those is that we're looking at unsatisfiability instead

of validity, right?

The only reason being is that there's a sense of direction kind of built in.

Instead of going from the axioms to the theorem A we want to prove, we go from the negation

of A to a contradiction.

And if you remember well, in resolution the contradiction was in the form of an empty

clause.

That gives us a tremendous notion of direction.

Small is beautiful, okay?

And the empty clause is the smallest possible one.

So that gives us the direction and that actually makes these things efficient.

Okay.

Yes.

The thing I would like to very briefly kind of alert you to is you remember that we did

tableau.

And tableau is essentially you start with A, label it by false and develop the whole

thing into a tree of possibilities and every one of these branches in my tree has to be,

has to contain a contradiction.

If you think about that, the branches internally I read as conjunctions, right?

If there's A, B, C and D on it, I read that as B, C and D. Whereas the branches are actually

act like an or.

So what we're actually implementing is something of the form I have a conjunction of literals

on each branch.

The others I don't want, the others are worked off, we talked about that.

Right?

And I have a big disjunction over that.

So I have something of that form.

And that's, we know that this always exists, it's called the disjunctive normal form and

we're implicitly computing that in a tableau and we are, if you want to think about it,

the inference process actually makes the contradictions that are already present in the original formula

A, we make them explicit, easy to detect.

The contradiction is if every possibility has a contradiction and how can a branch have

a contradiction?

Well, something and something and something and something and contradiction, well, that's

it.

In conjunction you have to make everything true and the contradiction you can never make

true.

So this is something you can actually see directly, you can write a three line program

that actually looks at a tableau, goes through recursively and looks for contradiction.

So it's in a way obvious.

And that's really all that inference procedures do.

We have a property of a formula or a description of the world that we're interested in and

we massage it into a form where that property becomes obvious and easy to read off.

That's how we do it in a tableau.