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.
978-3-642-38573-5
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11590/175254
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact