Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms (called nominals) and the so-called satisfaction operator, that allows one to state that a given formula holds at the world named a, for some nominal a. Hence, in particular, hybrid formulae include ``equality'' assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. This paper introduces an internalized tableau system for basic hybrid logic, significantly reducing such redundancies. The calculus enjoys a strong termination property: tableau construction terminates without relying on any specific rule application strategy, and no loop-checking is needed. The treatment of nominal equalities specific of the proposed calculus is briefly compared to other approaches. Its practical advantages are demonstrated by empirical results obtained by use of implemented systems. Finally, it is briefly shown how to extend the calculus to include the global and converse modalities.

CERRITO S., & CIALDEA MAYER M (2010). An efficient approach to nominal equalities in hybrid logic tableaux. JOURNAL OF APPLIED NON-CLASSICAL LOGICS, 20 (1-2), 39-61 [10.3166/jancl.20.39-61].

An efficient approach to nominal equalities in hybrid logic tableaux

CIALDEA, Marta
2010

Abstract

Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms (called nominals) and the so-called satisfaction operator, that allows one to state that a given formula holds at the world named a, for some nominal a. Hence, in particular, hybrid formulae include ``equality'' assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. This paper introduces an internalized tableau system for basic hybrid logic, significantly reducing such redundancies. The calculus enjoys a strong termination property: tableau construction terminates without relying on any specific rule application strategy, and no loop-checking is needed. The treatment of nominal equalities specific of the proposed calculus is briefly compared to other approaches. Its practical advantages are demonstrated by empirical results obtained by use of implemented systems. Finally, it is briefly shown how to extend the calculus to include the global and converse modalities.
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: http://hdl.handle.net/11590/140554
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact