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