 Modal logics find extensive use in computing science as logics of knowledge and belief, logics of programs, and in the specification of distributed and concurrent systems. Thus, a program that automates reasoning in a modal logic such as K, K4, T, S4, or S5 would have important applications. With the exception of S5, these logics share some of the important metatheoretical results of classical logic, such as cut-elimination, and hence cut-free (modal) sequent calculi can be provided for them, along with techniques for their automation. Connection methods (Andrews 1981, Bibel 1981) have played an important role in helping to understand the source of redundancies in the search space induced by these modal sequent calculi and have provided a unifying framework not only for modal logics but also for intuitionistic and classical logic as well (Wallen 1990). Current efforts to automate modal logic reasoning revolve around the translational approach mentioned above, namely to embed modal logic into classical logic and then use an existing automated reasoning system for the latter to prove theorems of the former. (Benzmüller &amp; Paulson 2013) shows how to embed quantified modal logic into simple type theory, proves the soundness and completeness of the embedding, and demonstrates with simple experiments how existing higher-order theorem provers can be used to automate proofs in modal logic. The approach can be extended to higher-order modal logic as well (Benzmüller &amp; Paleo 2015).