Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference

Mark Kaminski; Gert Smolka

Publication details

Programming Systems

Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference

Mark Kaminski, Gert Smolka

LPAR-17, Vol. 6397 of LNCS (ARCoSS), pp. 417-431, Springer, October 2010

We introduce the method of clausal graph tableaux at the example of hybrid logic with difference and star modalities. Clausal graph tableaux are prefix-free and terminate by construction. They provide an abstract method of establishing the small model property of modal logics. In contrast to the filtration method, clausal graph tableaux result in goal-directed decision procedures. Until now no goal-directed decision procedure for the logic considered in this paper was known. There is the promise that clausal graph tableaux lead to a new class of effective decision procedures.

Version with full proofs.
DOI (LNCS version): 10.1007/978-3-642-16242-8_30

Download PDF Show BibTeX

@INPROCEEDINGS{KaminskiSmolka:2010:ClausalGraph,
  title = {Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference},
  author = {Mark Kaminski and Gert Smolka},
  year = {2010},
  month = {Oct},
  editor = {Christian Fermüller and Andrei Voronkov},
  publisher = {Springer},
  booktitle = {LPAR-17},
  series = {LNCS (ARCoSS)},
  volume = {6397},
  pages = {417-431},
  note = {Version with full proofs.},
}

Legal notice, Privacy policy