Thread: Converting FOL with equality or not equal to clausal form

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

Originally Posted by helen2007

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?

Does FOL mean first order logic ?
If so, in what context, course, textbook, axiom system, or whatever are you using this?

Yes. It means First Order Logic. Currently I am reading the book Knowledge Representation and Reasoning. First Order Logic representations of the domain can be converted to clausal forms, and then resolution can be used to solve them.

Do I understand right that to convert a formula to clausal form you convert it to a prenex form, introduce Skolem constants and remove quantifiers, then convert the result to the conjunctive normal form? What difficulty do = and <> introduce compared to other predicate symbols? I think both of your formulas convert to (not p(X) \/ not p(Y) \/ X = Y).

Also, resolution is not an indispensable topic in first-order logic. There are many courses that don't cover it. However, it is more important in knowledge representation.

Thanks for the reply. I think your understanding is correct. I have read that = or <> require special handling, like using axioms of equality or Paramodulation. But I don't know how to apply those to my examples.

Isn't paramodulation an inference rule, just like resolution? It is something that is applied after you convert your formulas to clausal form.

Sorry ... I am not sure exactly what paramodulation is ......

Originally Posted by helen2007

Sorry ... I am not sure exactly what paramodulation is ......

That is the whole problem: neither do we, or at least I don't.
I have many many texts on set theory/logic but none have that term.
It is not a term even on Wikipedia.

Originally Posted by helen2007

I have read that = or <> require special handling, like using axioms of equality or Paramodulation. But I don't know how to apply those to my examples.

I think that the answer to your original question is in post #4. The special handling you are talking about refers not to converting formulas to clausal form, but to deriving an empty clause from a set of clauses. If a set of clauses is contradictory, i.e., it does not have any model, then resolution alone is capable of deriving an empty clause. However, it may be that a set of clauses has only models that do not satisfy the equality axioms. Then resolution alone cannot derive an empty clause. However, we would like to consider such set of clauses contradictory because we assume that equality is not an arbitrary predicate symbol but satisfies the equality axioms. Therefore, we need a stronger inference rule to derive an empty clause. As I understand it, resolution and paramodulation are able to derive an empty clause in this case.