A general framework for translating logical formulae from one logic into another logic is presented. The framework is instantiated with two different approaches to translating modal logic formulae into predicate logic. The first one, the well known ‘relational’ translation makes the modal logic‘s possible worlds structure explicit by introducing a distinguished predicate symbol to represent the accessibility relation. In the second approach, the ‘functional’ translation method, paths in the possible worlds structure are represented by compositions of functions which map worlds to accessible worlds. On the syntactic level this means that every flexible symbol is parametrized with particular terms denoting whole paths from the initial world to the actual world. The ‘target logic’ for the translation is a first-order many-sorted logic with built in equality. Therefore the ‘source logic’ may also be first-order function symbols are allowed. Furthermore flexible function symbols are allowed. The modal operators may be parametrized with arbitrary terms and particular properties of the accessibility relation may be specified within the logic itself.