Terminating tableau systems for hybrid logic with difference and converse (Q1047795)

The paper presents a tableau-based decision procedure for hybrid logic with global, difference, and converse modalities, considering also reflexive and transitive relations. The main contributions are a new model existence theorem, a terminating control that does not rely on the usual chain-based blocking scheme, a new treatment of the equational constraints that come with nominals and difference, and a terminating tableau for difference modalities.