Sciweavers

Share
CADE
2008
Springer

Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

9 years 2 months ago
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
Abstract. We present the first terminating tableau calculus for basic hybrid logic with the difference modality and converse modalities. The language under consideration is basic multi-modal logic extended with nominals, the satisfaction operator, converse, global and difference modalities. All of the constructs are handled natively. To obtain termination, we extend chain-based blocking for logics with converse by a complete treatment of difference. Completeness of our calculus is shown via a model existence theorem that refines previous constructions by distinguishing between modal and equational state equivalence. Key words: modal and hybrid logics, difference modality, converse, tableau systems, decision procedures
Mark Kaminski, Gert Smolka
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Mark Kaminski, Gert Smolka
Comments (0)
books