And then when we noticed that, we reconsidered and added two new rules which essentially,

and that's a very important thing in first order inference, allow us to postpone the

decisions on what the substitutions are.

At some point, you have variables, you need to substitute them, and if you substitute

early, you have very little information, if you substitute late, you may have more information.

That's what you hope for.

And the idea here is that you essentially, in the crucial step here, where you have to

substitute something, you don't actually, you substitute a variable for another.

Basically saying, oh yeah, I'll take some value y for this, and who knows what it's

going to be.

That's great, because this here doesn't have this combinatorial explosion of doing infinite

stuff.

You have to adapt to other rules here.

You have to make the witnesses we instantiated kind of depend on the three variables on later

decisions, and you have to adapt the closure rules where you actually take a substitution

that makes these two complementary literals the same.

And as we're going to see today, this here is something that is algorithmic.

This subproblem is, you can actually do algorithmically.

And that is a very, that's called unification, and unification is one of the basic CS algorithms.

And we understand it very well.

And it's at work in many things.

Right.

We looked at an example which revealed that even though in this rule we don't have immediate

infinite branching, but still we have to allow ourselves to apply this rule multiple times.

Okay.

So we're delaying choice, but we still have to choose how many times we're going to apply

this rule.

And that was kind of the idea here of this proof, which you can already see, right, P

of A or P of B implies there is an X, P of X.

Right.

Obviously.

Right.

Peter loves Mary or John loves Mary implies that somebody loves Mary.

Okay.

And there are kind of two cases why this could be true.

One is that it's Peter and one is that it's John.

And we have to kind of, that's the behavior we're expecting from that proof.

And we're getting that here in these two branches of the tableau, one of which we can close

right away, which puts us into the problem that after we've instantiated the whole tableau

with A for Y, which is by the way, a very important thing that is easily forgotten.

If you forget this, and I think in all of the final exams, two so far, and there's been

a tableau where you had to not forget that you're instantiating in this case, all the

Y's by A, giving you this thing here, right.

So we're here, we're stuck.

We don't have any literal up here that is complementary and that we can make complementary

to P of B.

Okay.

So what we need to do is we need to apply the rule here a second time, which gives me

a P of Z.

We have a P of B, P of Z, true and false.