Higher-order modal logic is a framework for modeling a large variety of problems and is applied in philosophy and computer science. Automating reasoning in this framework could be very beneficial. Unfortunately, there exists no software which achieves this. However automatic reasoning tools for higher-order logic do exist and there is a method which allows expressing higher-order model logic in terms of higher-order logic. Hence, the method enables automatic reasoning in the desired logic. In this thesis a tool which converts a higher-order model problem into a higher-order problem by applying this method is devised.