Arnon Avron, Furio Honsell, Marino Miculan and Cristian Paravano
Encoding Modal Logics in Logical Frameworks.
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.
Keywords: Hilbert and Natural-Deduction proof systems for
Modal Logics, Logical Frameworks, Typed lambda-calculus, Proof