Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

Mark Kaminski; Gert Smolka

Publication details

Programming Systems

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

@INPROCEEDINGS{KaminskiSmolka08converse,
  title = {Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse},
  author = {Mark Kaminski and Gert Smolka},
  year = {2008},
  month = {Aug},
  editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
  publisher = {Springer},
  booktitle = {IJCAR 2008},
  series = {LNCS (LNAI)},
  volume = {5195},
  pages = {210-225},
}

Legal notice, Privacy policy