 Gentzen and natural deduction systems for logics similar to hybrid logics were explored already in the 1990s by Jerry Seligman, see the overview in Seligman (2001). In particular, Seligman developed proof-systems that work with arbitrary formulas, not just satisfaction statements, the latter being the case for most proof-systems for hybrid logic, where satisfaction operators are used to access information hidden behind modalities. A natural deduction system in this style was introduced in Seligman (1997) and this system has been further developed in Chapter 4 of the book Braüner (2011a). A tableau systems in Seligman’s proof-style has been considered in Blackburn, Bolander, Braüner, and Jørgensen (2017) where a syntactic completeness proof is given. A semantic completenes proof of the tableau system is given in Jørgensen, Blackburn, Bolander, Braüner (2016). Reasoning in these systems does not directly rely on the global encodings that satisfaction operators make possible, hence, these systems can be considered more in line with the local character of the standard Kripke semantics for modal logic. In fact, this more local reasoning style makes these systems suitable for formalizing the perspectival reasoning taking place in certain psychological reasoning tasks, see Braüner (2014b) as well as Braüner, Blackburn, and Polyanskaya (2016).