This is an extended version of the lectures given during the 12-thConference on Applications of Logic in Philosophy and in the Foundationsof Mathematics in Szklarska Poręba. It contains a surveyof modal hybrid logic, one of the branches of contemporary modal logic. Inthe first part a variety of hybrid languages and logics is presented with adiscussion of expressivity matters. The second part is devoted to thoroughexposition of proof methods for hybrid logics. The main point is to showthat application of hybrid logics (...) may remarkably improve the situation inmodal proof theory. (shrink)

We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified (...) using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts. (shrink)

LF has been designed as a meta-logical framework to represent logics, and has become a standard tool for studying properties of logics. Building on the newly introduced module system for LF, we present the nucleus of an integrated and structured development of the syntax, semantics, and proof theory of logics, and of the relations between those logics. The methodology is chosen so that it will scale to an atlas for the zoo of logics currently used in reasoning systems, and the (...) modular nature of this development aids the practical integration of systems because shared features of the logics are reused directly. Finally we show how these encodings in LF are imported into the Hets system, which provides automated proof support on the modular level and integrates various automated theorem provers for the represented object logics. (shrink)