×

Multimodal and intuitionistic logics in simple type theory. (English) Zbl 1222.03023

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.

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)
PDFBibTeX XMLCite
Full Text: DOI Link