Deductive Systems and the Decidability Problem for Hybrid Logics

The book stands at the intersection of two topics: the decidability and computational complexity of hybrid logics, and the deductive systems designed for them. Hybrid logics are divided into two groups: standard hybrid logics involving nominals as expressions of a separate sort, and non-standard hybrid logics, which do not involve nominals but whose expressive power matches the expressive power of binder-free standard hybrid logics. The original results of the book are split into two parts. This division reflects the division of the book itself. We can say that the first type of results concern model-theoretic and complexity properties of hybrid logics. Since hybrid logics which we call standard are quite well investigated, our efforts focused on hybrid logics referred to as nonstandard in the book. By nonstandard hybrid logics we mean modal logics with global counting operators whose expressive power matches the expressive power of binder-free standard hybrid logics.