Model logic is a formalism suitable for modelling problems in artificial intelligence, computer science, philosophy and many other disciplines. Its automation in all its flavours can easily be achieved employing the semantic embedding approach and resuing existing reasoning software: This thesis presents a procedure that encodes a problem of higher-order modal logic in higher-order  logic which is implemented in the Model Embedding Tool for the input language TPTP THF which was extended for this purpose. By combining this software with one or more compliant reasoners a competitive system is created that can handle countless more variants of modal logic than any other theorem prover available to date.