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!


1 Answer 1


The variables called x in the two sentences are not related. We can rename them to make it clear:

~Loves(x1,F(x1)) v Loves(G(x1),x1)
~Animal(x2) v Loves(Jack,x2)

Now when matching ~Loves(x1,F(x1)) and Loves(Jack,x2), you can see you'll get Jack/x1, F(Jack)/x2 and the final result as in the book.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.