Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics

TL;DR

This paper develops sound and complete tableau calculi for two-dimensional hybrid product logic and hybrid dependent product logic, advancing formal reasoning methods for these complex modal systems.

Contribution

It introduces novel tableau calculi for two-dimensional HPL and HdPL, including a special rule for HdPL, ensuring soundness and completeness.

Findings

Constructed sound and complete tableau calculus for 2D HPL

Developed tableau calculus for HdPL with a new rule

All calculi lack termination properties

Abstract

Hybrid logic is one of the extensions of modal logic. The many-dimensional product of hybrid logic is called hybrid product logic (HPL). We construct a sound and complete tableau calculus for two-dimensional HPL. Also, we made a tableau calculus for hybrid dependent product logic (HdPL), where one dimension depends on the other. In addition, we add a special rule to the tableau calculus for HdPL and show that it is still sound and complete. All of them lack termination, however.