A formula of first-order logic is said to be in Skolemized form (sometimes also called Skolem standard form or universal form)
if it is of the form

where
is a quantifier-free formula in conjunctive
normal form known as the matrix of the formula in question. Since is a conjunction of clauses
each of which is a disjunction of literals,
is often viewed as a set of the clauses.
The process of placing a formula in Skolemized form is known as Skolemization.