Alternative translation techniques for propositional and first-order modal logics

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 square-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 square-as-Pow but is simpler and computationally more attractive. We also discuss the relationships between the two methods, showing that square-as-Pow generalizes to the first-order case. For first-order modal logics, we describe two extensions, of different degrees of generality, of square-as-Pow to logics of rigid designators and constant domains.