Conversion of a first-order formula into a conjunctive normal form involves removal of existential quantifications by Skolemization. Classical Skolemization, however, does not preserve the logical meaning of a formula. In this paper, we propose an extension of first-order formulas by incorporation of function constants and function variables. By applying function constants to ground arguments, syntactically different extended first-order terms may be evaluated into the same extended term. Extended terms thus constitute a quotient space. The resulting extended formula space allows meaning-preserving Skolemization by converting an existentially quantified usual variable into an extended term with an existentially quantified function variable. A procedure for transforming a first-order formula into an extended conjunctive normal form on the extended space is presented. [ABSTRACT FROM AUTHOR]