We postponed the quiz until 1705.

Somebody say that on the public channel as well.

Yeah, something.

So Abhishek is working and he thinks it will be done by then.

So let's talk about first order unification.

You're hearing me via the...

Okay, good.

Now it's working.

Okay, so we were...

Remember we were talking about tableaus and one of the problems for closing, meaning finding a literal A true and another literal A false,

well that doesn't work anymore because we had postponed decisions.

So really it's an A with a lot of variables and a B with a load of variables with different intended truth values.

And now we have the problem of making those two equal so that we can close.

And that's a problem you find in many places in computer science and the algorithm that solves that is called first order unification.

It was invented to do first order resolution, which is something we're going to come to,

but we're first going to do tableau and it actually works the same there.

Now, we looked at this problem of making two terms equal by a substitution and it turns out there are lots of solutions to this.

And we looked at...

We looked at and found out that there is a convenient notion of a most general unifier.

It is one that can be further instantiated to get any other unifier.

And we actually looked at the details here.

I'm not going to go over that.

And essentially the main thing here is we identified certain unification problems as solved forms.

And the idea is that we give ourselves a calculus that takes any unification problem,

you massage it with the calculus until you're in a solved form or in an unsolvable form.

And from the solved forms we can read off the most general unifier.

And from the unsolvable ones we can see that they're unsolvable.

And then the only thing you need is the calculus that massages the rules.

We have a decomposition rule that allows you to strip off the head symbol,

F in this case, compare the arguments pairwise.

You can delete trivial pairs.

And if you have a pair that looks, an equation that looks solved,

but which isn't because the X actually appears somewhere else,

then you can just turn this into a substitution and eliminate, hence the name, the X from the rest by replacing it by the right hand side.

We do all of this with the convention that we can reorder equations.

A and B is the same as B and A, which is why I chose the AND notation.

And that we can reorder the equalities from left to right, right to left, as we need it.

And we've started looking at the properties of this calculus.

One is that it's correct, meaning it doesn't invent any unifiers by the translation,

meaning the set of unifiers before the transformation is a subset of the,

is a superset of the set after and the other way around, which is completeness.

And I told you with a strong hint to actually look at it yourselves that this calculus is confluent,

meaning if I have a unification problem where I can apply two rules, then I can actually undo it, if you will.

The confluence is a property you see quite a lot in any kind of theoretical computer science.

So the idea is if you have a problem E and you can take one rule and make it into an E prime

and another rule to make it into an E double prime, you can actually come back together into a say E triple prime.

In confluence, even though we only have one step to go in different directions, you allow multiple steps to come back together.

An example of this, if you have, let me, x equals f of y, y, and what is it, y equals a,

and I don't know, f of y equals f of a or something like this.

If you eliminate, no, I probably need something, I should have thought about this example first.