2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/230501We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.ii + 22 pagesArtificial IntelligenceLogic in Computer ScienceI.2.4; I.2.3; F.4.1text