Terminating Tableaux for Hybrid Logic with Eventualities

Mark Kaminski; Gert Smolka

Publication details

Programming Systems

Terminating Tableaux for Hybrid Logic with Eventualities

Mark Kaminski, Gert Smolka

IJCAR 2010, Vol. 6173 of LNCS (LNAI), pp. 240-254, Springer, July 2010

We present the first terminating tableau system for hybrid logic with eventualities. The system is designed as a basis for gracefully degrading reasoners. Eventualities are formulas of the form <>*s that hold for a state if it can reach in n>=0 steps a state satisfying the formula s. The system is prefix-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision procedures.

DOI: 10.1007/978-3-642-14203-1_21

Download PDF Show BibTeX

@INPROCEEDINGS{KaminskiSmolka:2010:Hstar,
  title = {Terminating Tableaux for Hybrid Logic with Eventualities},
  author = {Mark Kaminski and Gert Smolka},
  year = {2010},
  month = {Jul},
  editor = {Jürgen Giesl and Reiner Hähnle},
  publisher = {Springer},
  booktitle = {{IJCAR} 2010},
  series = {LNCS (LNAI)},
  volume = {6173},
  pages = {240-254},
}

Legal notice, Privacy policy