Publication details

Saarland University Computer Science

A Straightforward Saturation-Based Decision Procedure for Hybrid Logic

Mark Kaminski, Gert Smolka

International Workshop on Hybrid Logic 2007 (HyLo 2007), August 2007

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

Legal notice, Privacy policy