Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

Abstract. We present the first terminating tableau calculus for basic hybrid logic with the difference modality and converse modalities. The language under consideration is basic multi-modal logic extended with nominals, the satisfaction operator, converse, global and difference modalities. All of the constructs are handled natively. To obtain termination, we extend chain-based blocking for logics with converse by a complete treatment of difference. Completeness of our calculus is shown via a model existence theorem that refines previous constructions by distinguishing between modal and equational state equivalence. Key words: modal and hybrid logics, difference modality, converse, tableau systems, decision procedures

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Mark Kaminski, Gert Smolka
• Keywords: Automated Reasoning, CADE 2008, Difference Modalities, Difference Modality, Terminating Tableau Calculus