Hello

New to the world of FOL. I have not been able to find a good tutorial on converting = or <> (not equal) signs in FOL when translating to clausal forms, and be grateful for your assistance.

Consider the following sentences (both about uniqueness):

1. for all X,Y p(X) and X<> Y -> not p(Y)

2. for all X,Y p(X) and p(Y) -> X=Y

assume my domin is D={a,b,c}

Could you tell me how could these be translated to clausal form?

Many thanks

P.S. This is not my homework! I am a graduate student and have to teach myself FOL