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方法的完备性定理与终止性质，进而验证了可判定性。