Two approaches to modal theorem proving are presented. The first approach is a direct one, developed specifically for modal logics. In the second approach a translation procedure is included and a classical first-order prover is used to the examined modal formulas. Some comparative results and possible extensions are discussed.