Citations of:
Add citations
You must login to add citations.


We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkinstyle completeness proofs even when the modal logic being hybridized is higherorder. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and firstorder hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of type $a$ that (...) 

Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms and the socalled satisfaction operator, that allows one to state that a given formula holds at the world named a, for some nominal a. Hence, in particular, hybrid formulae include “equality” assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. This paper (...) 

We show that basic hybridization makes it possible to give straightforward Henkinstyle completeness proofs even when the modal logic being hybridized is higherorder. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{69pt} \begin{document}$@_i$\end{document} in propositional and firstorder hybrid logic. This means: interpret \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{69pt} \begin{document}$@_i\alpha _a$\end{document}, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} (...) 

Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus T H(@,E,D, ♦ −) for hybrid logics with the satisfaction operators, the universal modality, the difference modality (...) 

