remembered my name before history shaggy

Our subject is more or less the completeness of the resolution method.

Last time we had developed this Abraham theory.

And we have shown the following completeness set.

As I said, this was already...

So, the one that says...

I'm sorry, I just have to shorten it.

The point G means quantity.

So, we take a quantity, a free formula.

You don't have to write it down, you already have it.

They are equivalent.

First, the universal conclusion of this formula is achievable, the formula that I get by making all the implicit quantifications of these free variables that occur, explicit.

Second, this universal conclusion has an error model, therefore error completeness.

And third, this quantity of the basic instances of this formula from the root of phi, E of phi, is logically achievable.

So, this is the reduction on this last point.

And third, this is the logical completeness of the quantity of the basic instances that now provide us with this completeness set for the resolution method.

By basically depicting a reduction of logic of the first step on statement logic.

Which will allow us to deduce the completeness of the resolution method in the predicate logic, on the completeness of this method in statement logic, which we already know.

So, what was the predicate logic resolution?

Well, it was the continued application of this rule resolution with implicit factoring.

I will write it down again.

So, here I have a clause that contains positive literals a1 to an.

Not to remember, this is now a saloppish writing method for a quantity c of literals, combined with a lot of inputs for this atom a1 to an.

So, here I have a clause that contains a negative literal, not b.

Then I unify through the bank.

And I expressly do this with the most general unifier, which means I make it as sparingly as possible.

Then I unify a1 to an and b.

This is a short writing method for any quantity of equations, which guarantees that everything will be the same. For example, all these a's are made b for i equal to 1 to n.

So, if I have all of them unified, then all of them fall into one.

They will all be the same.

And this one here is the negative of the one.

So, I can solve it correctly and everything that is explicitly represented here will fall away.

So, c sigma comma d sigma.

The a1 to an, you mean?

The a1 to an are atomic formulas, and b as well.

Let's leave the case with equality, because we have made this whole Erbran theory just for the case without equality.

So, they have this form here, predicate application on any terms e1 to ek.

This is an atomic formula in predicate logic. We are in predicate logic, an atomic formula.

So, it is either an equation, but we have excluded it, or a predicate application.

The predicate symbol k is applied here on terms e1 to ek.

And in these terms e1 to ek, of course, variables can be in there.

And by using these variables, something is unified.

I can't use constants. Consants are constants.

So, I can only unify the variables.

So, I can only use something in variables.

That is what is meant here.

And now we liberalize these rules.

And we call the resulting rule L-Riff, the liberalized resolution with implicit factoring.

And the difference is that we now allow sigma to be an arbitrary unifier from a1 to a n and b,

and no longer a general unifier.