Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
Provides formal proof systems for two-dimensional hybrid logics, addressing a gap in logical foundations for modal logic extensions.
The paper constructs sound and complete tableau calculi for two-dimensional hybrid product logic and hybrid dependent product logic, but these calculi lack termination.
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.