## Skolemization

Expand Messages
• 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, 2012
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?
• 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, 2012
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,

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)
>
>
>
>
>
> ------------------------------------------------------------------------