i have problem with resolution in first order logic

i have :

C1  :
¬ Loves(x,F(x) ) or Loves ( G(x) , x )


C2 : 

¬ Animal ( X) or Loves ( jack , x ) 

can some one help me why the answer ( after Resolve C1,C2 ) is :

¬ Animal(F(jack) ) or Loves ( G(jack) , jack )

because my answer is :

x/ jack

then i will have :

C1 : 
¬ Loves ( jack , F(jack ) ) or Loves ( G(jack),jack ) 

C2 : 

¬ Animal ( jack ) or Loves ( jack,jack ) 

and i cant use resolution with Loves (jack,jack) and ¬ Loves (jack,F(jack))

thank you all !!


1 Answer 1


If you want to resolve C1 with C2, then the only option is for Loves(jack, x) (in C2) to match ¬Loves(x, F(x)) (in C1), and so as you state, you should substitute x=jack in C1 and x=F(jack) in C2. Upon making these substitutions, C1 and C2 become:

C1[x/jack] = ¬Loves(jack, F(jack)) or Loves(G(jack), jack)

C2[x/F(jack)] = ¬Animal(F(jack)) or Loves(jack, F(jack))

Resolving the two, we get:

¬Animal(F(jack)) or Loves(G(jack), jack)


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.