Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy