Loading ...
Sorry, an error occurred while loading the content.

Skolemization

Expand Messages
  • BasmatiT
    I m struggling a bit with the implications of skolemization. AIMA writes that the skolemized sentence is satisfiable exactly when the original sentence is
    Message 1 of 2 , Apr 19 1:26 PM
    • 0 Attachment
      I'm struggling a bit with the implications of skolemization. AIMA writes that the skolemized sentence is "satisfiable exactly when the original sentence is satisfiable". How is that different from equivalence? In particular, if I express "someone is happy" as

      1. E x happy(x)

      the skolemized sentence is, taking X32 as my Skolem constant:

      2. happy(X32)

      and I'm okay with that. 2 looks very much "equivalent" to 1. But then I'll take the negations of both, to yield:

      1' ¬(E x happy(x))
      2. ¬(happy(X32))

      and suddenly, they don't look equivalent at all. The second sentence says that someone is unhappy, whereas the first one (correctly) says that nobody is happy.

      Now, of course, if one converts everything to CNF form and applies resolution normally, no such problem can arise, as negation is moved inward before introducing Skolem constants. However, I'm still uncomfortable applying Skolemization if it doesn't produce an equivalent sentence. Is there anything that I'm missing?
    • Adila Alfa Krisnadhi
      Skolemization works because what we compute with resolution is (un)satisfiability of the formula. So, it suffices to preserve satisfiability rather than
      Message 2 of 2 , Apr 20 6:13 AM
      • 0 Attachment
        Skolemization works because what we compute with resolution is
        (un)satisfiability of the formula.
        So, it suffices to preserve satisfiability rather than equivalence:

        Let F be the original formula and F' be the formula after skolemization.
        Then,

        F is (un)satisfiable iff F' is (un)satisfiable
        Also, F' is (un) satifiable iff resolution on F' terminates with empty clause.

        regards,
        Adila

        On Fri, Apr 20, 2012 at 3:33 AM, <aima-talk@yahoogroups.com> wrote:
        > There is 1 message in this issue.
        >
        > Topics in this digest:
        >
        > 1. Skolemization
        >    From: BasmatiT
        >
        >
        > Message
        > ________________________________________________________________________
        > 1. Skolemization
        >    Posted by: "BasmatiT" basmati.tremblay@... basmati.tremblay
        >    Date: Thu Apr 19, 2012 10:56 pm ((PDT))
        >
        > I'm struggling a bit with the implications of skolemization. AIMA writes that the skolemized sentence is "satisfiable exactly when the original sentence is satisfiable". How is that different from equivalence? In particular, if I express "someone is happy" as
        >
        > 1. E x happy(x)
        >
        > the skolemized sentence is, taking X32 as my Skolem constant:
        >
        > 2. happy(X32)
        >
        > and I'm okay with that. 2 looks very much "equivalent" to 1. But then I'll take the negations of both, to yield:
        >
        > 1' ¬(E x happy(x))
        > 2. ¬(happy(X32))
        >
        > and suddenly, they don't look equivalent at all. The second sentence says that someone is unhappy, whereas the first one (correctly) says that nobody is happy.
        >
        > Now, of course, if one converts everything to CNF form and applies resolution normally, no such problem can arise, as negation is moved inward before introducing Skolem constants. However, I'm still uncomfortable applying Skolemization if it doesn't produce an equivalent sentence. Is there anything that I'm missing?
        >
        >
        >
        >
        >
        >
        > Messages in this topic (1)
        >
        >
        >
        >
        >
        > ------------------------------------------------------------------------
        > Yahoo! Groups Links
        >
        >
        >
        > ------------------------------------------------------------------------
        >
      Your message has been successfully submitted and would be delivered to recipients shortly.