Publication details
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},
}
Login to edit
Legal notice, Privacy policy