Avron, Arnon; Honsell, Furio; Miculan, Marino; Paravano, Cristian Encoding modal logics in logical frameworks. (English) Zbl 0954.03021 Stud. Log. 60, No. 1, 161-208 (1998). Summary: We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deduction-style proof systems for representing both truth (local) and validity (global) consequence relations for various Modal Logics. We introduce several techniques for encoding the structural peculiarities of necessitation rules, in the typed \(\lambda\)-calculus metalanguage of the Logical Frameworks. These formalizations yield readily proof-editors for Modal Logics when implemented in Proof Development Environments, such as Coq or LEGO. Cited in 12 Documents MSC: 03B45 Modal logic (including the logic of norms) 03B35 Mechanization of proofs and logical operations 03B40 Combinatory logic and lambda calculus 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:proof assistants; formalizations of modal logics in logical frameworks; typed \(\lambda\)-calculus; proof development environments; type theories; proof systems; consequence relations; necessitation rules Software:leanTAP; Coq PDFBibTeX XMLCite \textit{A. Avron} et al., Stud. Log. 60, No. 1, 161--208 (1998; Zbl 0954.03021) Full Text: DOI