Results 1 to 9 of 9

Math Help - Converting FOL with equality or not equal to clausal form

  1. #1
    Newbie
    Joined
    Oct 2012
    From
    Canada
    Posts
    5

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor

    Joined
    Aug 2006
    Posts
    18,403
    Thanks
    1485
    Awards
    1

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

    Quote Originally Posted by helen2007 View Post
    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?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Oct 2012
    From
    Canada
    Posts
    5

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

    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.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,418
    Thanks
    718

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

    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.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Oct 2012
    From
    Canada
    Posts
    5

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

    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.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,418
    Thanks
    718

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

    Isn't paramodulation an inference rule, just like resolution? It is something that is applied after you convert your formulas to clausal form.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Oct 2012
    From
    Canada
    Posts
    5

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

    Sorry ... I am not sure exactly what paramodulation is ......
    Follow Math Help Forum on Facebook and Google+

  8. #8
    MHF Contributor

    Joined
    Aug 2006
    Posts
    18,403
    Thanks
    1485
    Awards
    1

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

    Quote Originally Posted by helen2007 View Post
    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.
    Follow Math Help Forum on Facebook and Google+

  9. #9
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,418
    Thanks
    718

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

    Quote Originally Posted by helen2007 View Post
    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Converting from Polar Form to Complex Form?
    Posted in the Trigonometry Forum
    Replies: 3
    Last Post: September 14th 2012, 04:18 AM
  2. Converting to Trigonometric form
    Posted in the Pre-Calculus Forum
    Replies: 1
    Last Post: November 3rd 2010, 04:49 AM
  3. Converting to Q = ae^kt form
    Posted in the Pre-Calculus Forum
    Replies: 2
    Last Post: March 1st 2010, 04:30 PM
  4. Converting from Polar form to Rectangular form
    Posted in the Calculus Forum
    Replies: 3
    Last Post: April 26th 2009, 10:47 PM
  5. Converting to and from polar form?
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: September 26th 2007, 03:10 PM

Search Tags


/mathhelpforum @mathhelpforum