Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@ARTICLE{KaSmoJoLLI2009,
  title = {Terminating Tableau Systems for Hybrid Logic with Difference and Converse},
  author = {Mark Kaminski and Gert Smolka},
  year = {2009},
  month = {Oct},
  journal = {Journal of Logic, Language and Information},
  volume = {18},
  pages = {437-464},
  number = {4},
}

Login to edit