LinkBack URL
About LinkBacksDoes FOL mean first order logic ?Originally Posted by helen2007
If so, in what context, course, textbook, axiom system, or whatever are you using this?
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
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.
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.
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.
  |
