 We treat quantified hybrid logics separately. First-order modal logic comes in many different versions, which also is the case with first-order hybrid logic. Tableau systems for first-order hybrid logic can be found in the paper Blackburn and Marx (2002). Natural deduction and axiom systems for first-order hybrid logic can be found in Chapter 6 of the book Braüner (2011a) and Chapter 7 of the book deals with natural deduction for intensional first-order hybrid logic. The paper Indrzejczak (2020) gives a Gentzen-style sequent calculus for first-order hybrid logic with lambda operators as well as existence and definedness predicates. The paper Barbosa, Martins, and Carreteiro (2014) gives an axiomatization of a fragment of first-order hybrid logic called equational first-order hybrid logic.