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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.