t. 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.
Cialdea, M. (2013). A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies. In Automated Deduction – CADE-24 (pp.76-90). BERLIN HEIDELBERG : Springer-Verlag [10.1007/978-3-642-38574-2_5].
A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
CIALDEA, Marta
2013-01-01
Abstract
t. 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
