Benzmüller, Christoph; Paulson, Lawrence C. Multimodal and intuitionistic logics in simple type theory. (English) Zbl 1222.03023 Log. J. IGPL 18, No. 6, 881-892 (2010). The authors extend an embedding of multimodal logics in simple type theory proposed by Brown in 2005. The starting point is a characterization of multimodal formulae as particular \(\lambda\)-terms in simple type theory. The authors show that this encoding is sound and complete. They illustrate that the encoding supports the formulation of meta-properties of encoded multimodal logics, such as the correspondence between certain axioms and properties of the accessibility relation \(R\), and show that some of these meta-properties can be efficiently automated within the higher-order theorem prover LEO-II.In addition, Gödel’s interpretation of propositional intuitionistic logic in modal logic is used for obtaining a sound and complete embedding of propositional intuitionistic logic in simple type theory. Reviewer: Viorica Sofronie-Stokkermans (Saarbrücken) Cited in 13 Documents MSC: 03B45 Modal logic (including the logic of norms) 03B15 Higher-order logic; type theory (MSC2010) 03B20 Subsystems of classical logic (including intuitionistic logic) 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:multimodal logic; intuitionistic logic; simple type theory; automated reasoning Software:TPS; ETPS; LEO-II; E Theorem Prover PDFBibTeX XMLCite \textit{C. Benzmüller} and \textit{L. C. Paulson}, Log. J. IGPL 18, No. 6, 881--892 (2010; Zbl 1222.03023) Full Text: DOI Link