 Natural deduction style proof-theory of hybrid logic has been explored in the book Braüner (2011a). This book also gives a cut-free Gentzen sequent system for hybrid logic. Cut-freeness is proved via a normalizing natural deduction system, but such a result can also be proved directly, see Indrzejczak (2016). The natural deduction and Gentzen systems of Braüner (2011a) can be extended with additional proof-rules corresponding to first-order conditions on the accessibility relations expressed by so-called geometric theories (this is of course analogous to extending tableau and axiom systems with pure axioms). See also Braüner and de Paiva (2006) where a natural deduction system is given for intuitionistic hybrid logic (Chapter 8 of Braüner (2011a)).