Publication details

Saarland University Computer Science

Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

Mark Kaminski, Gert Smolka

IJCAR 2008, Vol. 5195 of LNCS (LNAI), pp. 210-225, Springer, August 2008

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.

DOI: 10.1007/978-3-540-71070-7_18

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009