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.

翻译：混合逻辑是一种具有额外算子以指定命名子的模态逻辑，其表达能力极强。例如，在基本模态逻辑中不存在对应于克里普克框架自反性的公式，但在混合逻辑中则存在此类公式。自反性之所以重要，是因为从图论视角审视时，自反且对称的克里普克框架可视为无向图。因此，研究具有对应于自反性与对称性公理的混合逻辑，有助于阐明无向图的逻辑性质。本文为无向图的混合逻辑构建了Tableau方法。我们的主要成果是证明了该Tableau方法的完备性定理与可终止性，从而推导出可判定性。