Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy