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.
