How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?
-
04-11-2019 - |
Question
I'm working on a program which must use inference in first-order logic, and everything is working great except for 1 thing which I don't understand.
The book I'm using, "Artificial Intelligence A Modern Approach" by Russell and Norvig, shows a proof on page 349 which has me confused.
They combine the two following sentences:
~Loves(x,F(x)) v Loves(G(x),x)
~Animal(x) v Loves(Jack,x)
And they combine into:
~Animal(F(Jack)) v Loves(G(Jack),Jack)
This makes absolutely no sense to me because the variable "x" becomes both "F(Jack)" and "Jack", and that seems wrong to me.
Using the Unify function which I created by following the pseudocode provided in the book returns a failed substitution, but if the combination of the previously mentioned sentences is correct then what kind of substitution would need to be returned? (I know it's not just {x/Jack} because that would result in the sentence "~Animal(Jack) v Loves(G(Jack),Jack)", Animal would be missing the function F as shown in the example.)
Any help would be extremely appreciated!
No correct solution