 Also the weaker hybrid logic obtained by omitting both of the binders \(\mathtt{\downarrow}\) and \(\mathtt{\forall}\) has been the subject of extensive exploration. It turns out that this binder-free logic and a number of variants of it are decidable. In the paper Areces, Blackburn, and Marx (1999), a number of complexity results are given for hybrid modal and tense logics over various classes of frames, for example arbitrary, transitive, linear, and branching. It is remarkable that the satisfiability problem of the binder-free hybrid logic over arbitrary frames is decidable in PSPACE, which is the same as the complexity of deciding satisfiability in ordinary modal logic. Thus, hybridizing ordinary modal logic gives more expressive power, but the complexity stays the same. Some work has been carried out on simulating nominals inside modal logic, see Kracht and Wolter (1997).