This work is a brief presentation of an extension of the proof procedure for a decidable fragment of hybrid logic presented in a previous paper. It shows how to extend such a calculus to multi-modal logic enriched with transitivity and relation inclusion assertions. A further result reported in this work is that the logic extending the considered fragment with the addition of graded modalities has an undecidable satisfiability problem, unless further syntactical restrictions are placed on their use.

Cialdea, M. (2014). Extended Decision Procedure for a Fragment of HL with Binders. JOURNAL OF AUTOMATED REASONING, 53(3), 305-315 [10.1007/s10817-014-9307-z].

Extended Decision Procedure for a Fragment of HL with Binders

CIALDEA, Marta
2014-01-01

Abstract

This work is a brief presentation of an extension of the proof procedure for a decidable fragment of hybrid logic presented in a previous paper. It shows how to extend such a calculus to multi-modal logic enriched with transitivity and relation inclusion assertions. A further result reported in this work is that the logic extending the considered fragment with the addition of graded modalities has an undecidable satisfiability problem, unless further syntactical restrictions are placed on their use.
2014
Cialdea, M. (2014). Extended Decision Procedure for a Fragment of HL with Binders. JOURNAL OF AUTOMATED REASONING, 53(3), 305-315 [10.1007/s10817-014-9307-z].
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/140810
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 2
social impact