Skolemizing
Skolemizing is a process in first-order logic used to eliminate existential quantifiers from a formula. It achieves this by replacing the existentially quantified variables with new function symbols, called Skolem functions. The arity of a Skolem function depends on the number of universally quantified variables that precede the existential quantifier. Specifically, if an existential quantifier is nested within one or more universal quantifiers, the Skolem function will take as arguments the variables of those preceding universal quantifiers. If an existential quantifier is not nested within any universal quantifiers, it is replaced by a constant symbol, which can be considered a Skolem function of arity zero.
The primary purpose of Skolemization is to transform formulas into a form that is easier to handle,