  A converter from first-order modal logics to classical higher- order logic is
presented. This tool enables the application of off-the-shelf higher-order
theorem provers and model finders for reasoning within first- order modal
logics. The tool supports logics K, K4, D, D4, T, S4, and S5 with respect to
constant, varying and cumulative domain semantics.
