Publication details

Saarland University Computer Science

Terminating Tableau Systems for Hybrid Logic with Difference and Converse

Mark Kaminski, Gert Smolka

Journal of Logic, Language and Information 18(4):437-464, October 2009

This paper contributes to the principled construction of tableau-based decision procedures for hybrid logic with global, difference, and converse modalities. We also consider reflexive and transitive relations. For converse-free formulas we present a terminating control that does not rely on the usual chain-based blocking scheme. Our tableau systems are based on a new model existence theorem.

DOI: 10.1007/s10849-009-9087-8

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy