Skolemized Form

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.