Abstract The widespread use of non-classical logics in Artificial Intelligence makes it desirable to have automated deduction methods (and in particular resolution methods) for these logics at our disposal. In this chapter we present several automated deduction methods for modal logics. We focus on the problems of normal forming and variable skolemization, which prove to be harder than in classical logic because of the enriched language. In particular we study a special type of modal logics called deterministic logics which provide a very general framework for these deduction methods. Their semantics are based upon access functions instead of accessibility relations. That allows us to refer explicitly to possible worlds. For these logics several difficult problems, like the existence of normal forms, can be solved in a very simple way, by skolemizing modal operators.