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.
New to topics? Read the docs here!