2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/231455In a case study we investigate whether off the shelf higher-order theorem provers and model generators can be employed to automate reasoning in and about quantified multimodal logics. In our experiments we exploit the new TPTP infrastructure for classical higher-order logic.ii + 30 pagesArtificial IntelligenceLogic in Computer ScienceI.2.4; I.2.3; F.4.1text