Hubert and Natural-Deduction proof systems for Modal Logics; Logical Frameworks; Proof Assistants; Typed a-calculus

We present and discuss various formal]zations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hubert- and Natural Deductionstyle proof systems for representing both truth (local) and validity (global) consequence …