Re: SUO: Re: clausal normal form and skolemization
Chris,
Yes, I just omitted the step of actually doing the
substitution of f(x) for y, which was the whole point of
the exercise.
John
>> Skolemization is a formal technique used in various operations
>> in theorem proving, consistency checking, and finding abstract
>> models. If you try to Skolemize an abstract formula, e.g.,
>>
>> (Ax)(Ey)p(x,y)
>>
>> the only thing you get is an unspecified function: y=f(x).
>
>John, just to be clear although "you get" such a function by Skolemization
>in place of the existential quantifier, in place of the entire sentence
>(Ax)(Ey)p(x,y) "you get" p(x,f(x)). Right?
>
>-chris
>