Complete and Terminating Tableau Calculus for Undirected Graph

TL;DR

This paper forms the tableau method of the hybrid logic for undirected graphs and shows the completeness theorem and the termination property of the tableau method, which leads to prove the decidability.

Abstract

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.

Figures (6)

• Figure 1: The rules of $\mathbf{TAB}$
• Figure 2: Non-terminating tableau of $\mathbf{TAB}$ with only $[\square_{\mathit{sym}}]$
• Figure 3: A closed tableau owing to $(\mathcal{I})$
• Figure 4: The model $\mathcal{M}_\Theta$ constructed from a branch $\Theta$ in Figure \ref{['tabsym']}
• Figure 5: The bulldozed model $\mathcal{M}_\Theta^B$ constructed from a branch $\Theta$ in Figure \ref{['tabsym']}

Theorems & Definitions (54)

• definition 1: language
• definition 2
• definition 3
• definition 4
• definition 5
• definition 6
• definition 7
• definition 8: probability
• theorem 1: termination
• theorem 2: completeness