# Some confusing steps with Resolution by refutation FOL

Here is the thing..

There are two step that confuses me In the famous example "Everyone who loves all animals is loved by someone etc..." We need to prove that who killed the cat "curiosity or jack" AI a modern approach 3rd edition.

Here are the two statements that confuses me

1- ¬Loves(x,F(x)) ∨ Loves(G(x),x)

2- ¬ animal(x) ∨ loves(Jack,x)

In order to get rid of ¬Loves(x,F(x)) we have to substitute {x/jack,F(x)/x} So the first statement becomes ¬Loves(jack,jack) ∨ Loves(G(jack),jack)

But the second statement becomes ¬animal(F(jack)) ∨ Loves(jack,jack)?

Why the predicate animal becomes ¬animal(F(jack)) instead of ¬animal(jack)?

The other thing that confuses me are these two statements

1- ¬Animal(F(Jack)) ∨ Loves(G(Jack),Jack)

2- Animal(F(x)) ∨ Loves(G(x),x)

To get rid of Animal(F(x)) we substitute {x/jack}, but then the statement becomes Loves(G(jack),jack)? What about the other Predicate Loves(G(Jack),Jack), shouldn't the statement becomes Loves(G(jack),jack) ∨ Loves(G(Jack),Jack)?

See page 349.

We have to substitute first $F(x)$ in place of $X$ (i.e. $\{ x/F(x) \}$) in 2) to get :

2') $¬Animal(F(x)) ∨ Loves(Jack, F(x))$.

Then we substitute $Jack$ in place of $x$ in both 1) and 2') to get :

1') $¬Loves(Jack,F(Jack)) ∨ Loves(G(Jack),Jack)$

2'') $¬Animal(F(Jack)) ∨ Loves(Jack, F(Jack))$.

Now we apply resolution to get :

3)$¬Animal(F(Jack)) ∨ Loves(G(Jack),Jack)$.

The next step uses :

4) $Animal(F(x)) ∨ Loves(G(x),x)$.

In order to unify it with 3) we have simply to perform the substitution $\{ x/Jack \}$ and then apply resolution to get :

5) $Loves(G(Jack),Jack)$

and we can simplify it because $p \lor p \equiv p$.