A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies

Marta Cialdea Mayer

Abstract. A tableau calculus constituting a decision procedure for hybrid logic with the converse modalities, the global ones and a restricted use of the binder has been defined in a previous paper. This work shows how to extend such a calculus to multi-modal logic equipped with two features largely used in description logics, i.e. transitivity and relation inclusion assertions. An implementation of the proof procedure is also briefly presented, along with the results of some preliminary experiments.

LNAI 7898, p. 76 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013