In this paper we present a saturation-based decision procedure for basic hybrid logic extended with the universal modality. Termination of the procedure is guaranteed by constraints that are conceptually simpler than the loop-checks commonly used with related tableau-based decision methods in that they do not rely on the order in which new formulas are introduced. At the same time, our constraints allow us to limit the worst-case asymptotic complexity of the procedure more tightly than it seems to be possible for methods using conventional loop-checks. The procedure is based on Hardt and Smolka's higher-order formulation of hybrid logic.
Download PDF Show BibTeX
Login to edit