Hybrid Tableaux for the Difference Modality

Mark Kaminski; Gert Smolka

Publication details

Programming Systems

Hybrid Tableaux for the Difference Modality

Mark Kaminski, Gert Smolka

M4M-5, Vol. 231 of ENTCS, pp. 241-257, Elsevier, March 2009

We present the first tableau-based decision procedure for basic hybrid logic with the difference modality. The decision procedure is gracefully degrading in that the less expressive constructs don't pay for the computationally expensive difference modality. The procedure can be specialized to reflexive and transitive frames. Key features of our approach are nominal elimination, pattern-based blocking, and expansion control.

DOI: 10.1016/j.entcs.2009.02.039

Download PDF Show BibTeX

@INPROCEEDINGS{KaminskiSmolka07difference,
  title = {Hybrid Tableaux for the Difference Modality},
  author = {Mark Kaminski and Gert Smolka},
  year = {2009},
  month = {Mar},
  editor = {Carlos Areces and St\'ephane Demri},
  publisher = {Elsevier},
  booktitle = {M4M-5},
  series = {ENTCS},
  volume = {231},
  pages = {241-257},
}

Legal notice, Privacy policy