Complete and Terminating Tableau Calculus for Undirected Graph

TL;DR

This paper develops a complete and terminating tableau calculus for hybrid logic with axioms for undirected graphs, establishing decidability and logical properties of such graph structures.

Contribution

It introduces a novel tableau calculus for hybrid logic tailored to undirected graphs, proving its completeness and termination.

Findings

The tableau calculus is complete for hybrid logic with undirected graph axioms.

The tableau calculus terminates, ensuring decidability.

The method provides a logical framework for analyzing undirected graphs.

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.