Skolemization refers to the practice of implementing formulas that use existential quantification by replacing existentially quantified variables with special terms that use skolem functions and are a function of the other variables in the rule. It can also refer to what happens when one of these rules fires: a new constant is generated, or skolemized.
