To achieve efficient proof procedures for quantificational logics with finitely many truth values we extend the classical resolution principle. By generalizing the notion of a semantic tree we demonstrate the completeness of resolution and of some effective refinements. We also present translation calculi that convert formulae of many valued logics to clause syntax. As an application we investigate some well known examples of many-valued logics.