Tableau Calculi for Hybrid Logics

Hybrid logics were proposed in 15 as a way of boosting the expressivity of modal logics via a novel mechanism: adding labels for states in Kripke models and viewing these labels as formulae. In addition, hybrid logics may contain quanti ers to bind the labels. Thus, hybrid logics have both Kripke semantics and a rst-order binding apparatus. We present pre xed tableau calculi for weak hybrid logics proper fragments of classical logic as well as for hybrid logics having full rst-order expressive power, and give a general method for proving completeness. For the weak quanti er-free logics we present a tableau-based decision procedure.

• Type: Conference
• Year: 1999
• Where: TABLEAUX
• Authors: Miroslava Tzakova
• Keywords: Artificial Intelligence, Hybrid Logics, Modal Logics, TABLEAUX 1999, Weak Hybrid Logics