  Hybrid logic is a modal logic with additional operators specifying nominals
and is highly expressive. For example, there is no formula corresponding to the
irreflexivity of Kripke frames in basic modal logic, but there is in hybrid
logic. Irreflexivity is significant in that irreflexive and symmetric Kripke
frames can be regarded as undirected graphs reviewed from a graph theoretic
point of view. Thus, the study of the hybrid logic with axioms corresponding to
irreflexivity and symmetry can help to elucidate the logical properties of
undirected graphs. In this paper, we formulate the tableau method of the hybrid
logic for undirected graphs. Our main result is to show the completeness
theorem and the termination property of the tableau method, which leads us to
prove the decidability.
