In this paper we give an overview of a selection of proof systems for propositional modal logics, namely, standard tableaux, modal KE tableaux, modal resolution and translation-based resolution. We will concentrate on translation-based resolution methods describing different translation-methods and various refinements of resolution. We also discuss how tableaux and modal resolution methods can be simulated in the general framework of resolution. [an error occurred while processing this directive]