 For formulas already expressed in standard logic notation, there is a systematic two-step procedure for transforming them into conjunctive normal form. The first step consists in re-expressing a formula into a semantically equivalent formula in prenex normal form, (Θx1)…(Θxn)α(x1,…,xn), consisting of a string of quantifiers (Θx1)…(Θxn) followed by a quantifier-free expression α(x1,…,xn) called the matrix. The second step in the transformation first converts the matrix into conjunctive normal form by using well-known logical equivalences such as DeMorgan’s laws, distribution, double-negation, and others; then, the quantifiers in front of the matrix, which is now in conjunctive normal form, are dropped according to certain rules. In the presence of existential quantifiers, this latter step does not always preserve equivalence and requires the introduction of Skolem functions whose role is to “simulate” the behaviour of existentially quantified variables. For example, applying the skolemizing process to the formula