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.