How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?

cs.stackexchange https://cs.stackexchange.com/questions/65827

  •  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

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top