This paper deals with resolution theorem proving in many-valued logic. The latter has found increasing applications in such diverse fields as nonmonotonic reasoning, error-correcting codes, and software/hardware verification. Here, very long nonclausal formulae naturally come out, and efficient normal form reductions are, if not a \textit{sine qua non}, at least a very interesting tool for the algorithmic manipulation of these formulas. The author develops a satisfiability preserving CNF reduction of formulas in finite-valued calculi. Generalizing Tseitin's structure preserving clause forms, and adapting the notion of polarity to the many- valued case, he is able to keep the length of the resulting formulas polynomially bounded with respect to the length of the input formulas, while avoiding the generation of redundant clauses. Formulas are labelled by signs which, in contrast to the two-valued case, are sets of truth values, rather than truth values. The author compares his work with previous results on many-valued normal forms by Baaz, Carnielli, Fernmüller, Morgan, Murray, O'Hearn, Orlowska, Rosenthal, Stachniak, and others. In a final section he discusses applications of his techniques to the many-valued counterparts of the existential and universal quantifiers.