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.
Download PDF Show BibTeX
Login to edit