We describe and analyze techniques, other than the standard relational/functional methods, for translating validity problems of modal logics into first-order languages. For propositional modal logics we summarize the Box-as-Pow method, a complete and automatic translation into a weak set theory, and then describe an alternative method, which we call algebraic, that achieves the same full generality of Box-as-Pow but is simpler and computationally more attractive. We also discuss the relationships between the two methods, showing that Box-as-Pow generalizes to the first-order case. For first-order modal logics, we describe two extensions, of different degrees of generality, of Box-as-Pow to logics of rigid designators and constant domains.
