OK, so in this module, we are going
to be talking about the resolution for first order
logic.
This is an optional module, but I
think it would be interesting to think about how we could apply
a resolution when we have this more complicated logic,
this first order logic.
And so far, we have talked about syntax, semantics,
we have talked about modus ponens,
when we have Horn clauses in first order logic.
And now we want to extend this, the idea of applying
inference rules, to settings where we don't necessarily
have Horn clauses.
So if you think about first order logic,
it's not really limited to settings
where we have Horn clauses.
We sometimes have non-Horn clauses.
Here is actually an example.
For all x x is student, this implies x knows some y.
OK?
So this some y, does there exist y here,
is going to create a non-Horn clause.
And why is that?
Because an existential quantifier is
really a glorified "or," right?
Like it's a glorified disjunction.
So what this is basically getting us is
knows x and y1 or x, y2, and so on.
And this basically creates an "or"
on this side of the implication.
And that makes this particular statement a non-Horn clause OK?
So what does that mean?
That means that I can't just apply modus ponens on it, OK?
So what can we do here?
So the high level strategy here is that we have this formula.
We have this first order logic formula.
First off, we need to convert it to a CNF form, new form,
to a conjunctive normal form.
And this is similar to before.
Like before, even in propositional logic,
when we had something that wasn't a Horn clause,
we were starting with writing it as a CNF form.
OK?
And then after that, we repeatedly
apply resolution rule on it.
And our resolution rule here is going
to be slightly different from the resolution rule
that we had in propositional logic,
because similar to modus ponens, we need to do unification.
We need to do substitution.
And similarly, we change our resolution rule
to actually have that element of unification and substitution
here, OK?
Converting to CNF is also not exactly
like we did converting to CNF in propositional logic.
There are going to be a few new things
that I'm going to attempt to give you some ideas around it.
But in general, I'm just giving like a high level strategy
idea of how you're going to apply resolution
to first order logic.
This is not a very complete explanation of that.
And in general it gets a little bit messy,
like when you think about applying resolution
to first order logic.
So think of this as a big picture,
like high level strategy and overview
for applying resolution here, OK?
All right, so let's start with a formula.
Let's say this is our formula.
And we have for all x, for all y, and y
is an animal implies x loves y.
And that implies that there exists
in y such that y loves x.
OK?
So this is some statement, some formula.
And what we would like to do is we would like
to convert this to a CNF form.
So how does a CNF form look like in first order logic?
So at the end of the day, the output
is going to look something like this for us.
So it's going to be an and of a bunch of clauses.
So these are clauses because they have "or's" between them.
And in addition to that, we have these new functions,
these capitalized Y or capitalized Z.
And these are called Skolem functions.
And I'm going to talk about what they are in a few slides, OK?
So there are a few things that are new, when
we think about the CNF form.
The first thing is that all variables
that I have in this form are actually like universally
quantified.
So there is like a for all x, that exists here,
that I have just dropped, OK?
So then in reality there is a for all x that exists here.
And then there are these Skolem functions
that are functions of things that are existentially
quantified, right?
So basically they represent existential quantifiers here.
And they're functions of this x thing that has a for all x
at the beginning on it.
OK?
So those are kind of like two new things that are happening,
in order to get a CNF form of this first order logic formula.
Let's actually go through an example for this.
So let's start with this statement
that says anyone who likes all animals is liked by someone.
OK?
So one can write this as an input that
says for all x, for all y, y is an animal implies x plus y,
and that full thing implies that there exists a y.
So y loves x, OK?
All right, so first thing to do is, similar to before,
if you want to follow like the steps of converting this
to a CNF form, we are going to eliminate implication.
So I'm going to eliminate this outside implication.
How do I eliminate it?
I'm going to take the negation of what comes before it.
So negation, up until here, or the rest of the statement.
I'm also going to replace this implication
by negation of the first part or the second part, so negation
of the first part or the second part.
And we get this statement, OK?
Now I'm going to push negations inwards
and eliminate double negations.
This is exactly what we have done before.
So let me push negations inside.
And it goes all the way to negation of love.
And now we have ended up with this formula, where we
have these quantifiers, right?
Like we have these for all under exist, and so on.
And everything else is an atomic formula, right?
Remember before, like when we were trying to convert things
to a CNF form, we would end up with propositional symbols,
right?
So we would have, you'd end up with propositional symbols
that could take a positive or a negative value, right?
So we would have positive or negative literals
at the end of the day.
But here we have atomic formulas.
So we end up with these atomic formulas, or negations
of these atomic formulas, OK?
So now one thing that is new is we're
kind of standardizing the variables here.
So we have a y here, and we have a y here.
But there is this existential quantifier on each of them.
And these y's are kind of treated as a local variable.
So in order to kind of like avoid confusion,
you're going to define like a new variable for each of them.
So I'm going to define a z here and keep this as y.
And, again, the reason I'm doing this is, at the end of the day,
I'm removing this for all x.
And I want to make sure that this y is a function of x.
And this z is a function of x.
And these are different things.
These are two different local variables, OK?
All right, so this is new.
So on the standardizing variables,
this is a new step that is done here, OK?
Now that we are left with this formula, what
we are going to do is we're going to replace all
these existentially quantified variables with something that's
called the Skolem function, OK?
So before we had there exists a y,
and this there exists a y depends on x2, right?
So for all x there exists a y.
So this is really a function of x, the Skolem function, the y
function of x.
The Skolem function is y function
of x, where z is a function of x.
So I'm going to write these Skolem functions
as functions of this variable, that is universally quantified.
And then I'm going to just drop that.
I'm going to later on drop this for all x,
so that that makes my life easier.
And then finally, I need to distribute or over
and, so I can end up with clauses
in conjunctive normal form.
And this is a similar step that we
have had before in propositional logic,
and remove the universal quantifiers.
And this is what I would end up having.
So now I've ended up with the formula in CNF form
in first order logic.
OK?
So just to recap what is new in it,
we have Skolem functions, which kind of
represent existential quantifiers and variables that
are universally quantified.
I've also dropped the universal quantifier on all my variables
here, OK?
So that those are kind of like the core differences here, OK?
So now we are ready to talk about resolution.
Now that we can write our formulas,
our first order logic formulas in CNF form,
then we can write the resolution rule as follows.
So we have these atomic formulas,
f1 or through fn or p.
And then we have another thing in our set of premises,
negation of q of or g1 through gm.
And notice that p and q could be different things,
because they might just look different from each other.
So what we do is we unify p and q.
And when we unify p and q, we get a substitution rule theta.
And then what we can actually infer,
what we can derive here from resolution,
is going to be an or of f1 or'd all the way
through fn or g1 all the way through gm.
We are basically canceling out p and q with each other.
But the reason we can do that is we
have unified p and q with the substitution rule theta.
So in this new formula, we are substituting
theta in the formula.
This is kind of similar to the substitution and unification
that we did in modus ponens.
We are just doing this now on resolution on these CNF clauses
that we have just created.
OK?
Let's give an example here.
So let's say that I have two CNF clauses here.
So I have animal y of x or loves z of x x.
And then I have negation of loves u and v,
or feeds u and v. OK?
So loves and negation of loves are the things
that I would like to be able to do unification on.
So if I unify these two, then I'm
going to come up with a substitution rule that
says substitute variable u, which
functions Z of x, substitute the variable v, with variable x,
OK?
And at the end of the day, the thing that I am inferring,
I'm deriving here, is going to basically cancel out these two.
And it's going to get animal y of x or feeds u and v.
But I'm not going to put u and v in there anymore.
Why is that?
Because I'm substituting this theta,
I'm substituting z of x for u and x
for v. So the thing that, at the end of the day,
I'm proving is animal y of x or feeds to Z of x x.
OK, so there's quite a bit of like simple manipulation
going on here.
But you kind of like get the gist of it.
It's very similar to resolution that we have seen so far,
combined with unification and substitution
over these new clauses, these new CNF clauses,
that we have talked about.
And that summarizes how we do inference of using resolution
in first order logic.