 Tableau, Gentzen, and natural deduction style proof-theory for hybrid logic work very well compared to ordinary modal logic. Usually, when a modal tableau, Gentzen, or natural deduction system is given, it is for one particular modal logic and it has turned out to be problematic to formulate such systems for modal logics in a uniform way without introducing metalinguistic machinery. This can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of uniform tableau, Gentzen, and natural deduction systems for wide classes of logics. The paper Blackburn (2000) introduces a tableau system for hybrid logic that has this desirable feature: Analogous to the axiom system of Blackburn and Tzakova (1999), completeness is preserved if the tableau system is extended with a set of pure axioms, that is, a set of pure formulas that are allowed to be added to a tableau during the tableau construction. The tableau system of Blackburn (2000) is the basis for a decision procedure for the binder-free fragment of hybrid logic given in Bolander and Braüner (2006). This line of work has been continued in the papers Bolander and Blackburn (2007) and Bolander and Blackburn (2009). The paper Cerrito and Cialdea (2010) presents another tableau-based decision procedure for hybrid logic. Other decision procedures for hybrid logics, which also are based on proof-theory, are given in the paper Kaminski and Smolka (2009). The procedures of the latter paper are based on a higher-order formulation of hybrid logic involving the simply typed lambda calculus.