This paper describes our approach to modal theorem proving. We make use of a first-order theorem prover SPASS and a translation of modal logics to path logics via the optimised functional translation. Path logics are clausal logics over the language of the monadic fragment of sorted first-order logic with a special binary function symbol for defining accessibility. Clauses of path logics are restricted in that only Skolem terms which are constants may occur and the prefix stability property holds. Ordinary resolution without any refinement strategies is a decision procedure for the path logics associated with K(m) and KT(m). Our decision procedure for S4 uses an a priori term depth bound. SPASS uses ordered resolution and ordered factoring, it supports splitting and branch condensing (splitting amounts to case analysis while branch condensing resembles branch pruning in the Logics Workbench), it has an extensive set of reduction rules including tautology deletion, subsumption and condensing, and it supports dynamic sort theories by additional inference and reduction rules.