International Symposium on Multiple-valued Logic, 1999 Bernhard Beckert, Reiner Hähnle, Felip Manya In the last years two automated reasoning techniques for clause normal form arose in which the use of labels are prominently featured: signed logic and annotated logic programming, which can be embedded into the first. The underlying basic idea is to generalise the classical notion of a literal by adorning an atomic formula with a sign or label which in general consists of a possibly ordered set of truth values. In this paper we relate signed logic and classical logic more closely than before by defining two new transformations between them. As a byproduct we obtain a number of new complexity results and proof procedures for signed logics.