Skolemization
= Skolemization
{c}
Replacing an existentially quantified variable by a fresh <Skolem function> of the preceding universally quantified variables. A witness independent of all universal variables is represented by a fresh constant. The operation preserves satisfiability after expanding the <first-order signature>; it is not generally <logical equivalence> for arbitrary interpretations of the new symbols.