We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system.

On the mosaic method for many-dimensional modal logics: a case study combining tense and modal operators

VIGANO', Luca;VOLPE, Marco
2013

Abstract

We present an extension of the mosaic method aimed at capturing many-dimensional modal logics. As a proof-of-concept, we define the method for logics arising from the combination of linear tense operators with an “orthogonal” S5-like modality. We show that the existence of a model for a given set of formulas is equivalent to the existence of a suitable set of partial models, called mosaics, and apply the technique not only in obtaining a proof of decidability and a proof of completeness for the corresponding Hilbert-style axiomatization, but also in the development of a mosaic-based tableau system. We further consider extensions for dealing with the case when interactions between the two dimensions exist, thus covering a wide class of bundled Ockhamist branching-time logics, and present for them some partial results, such as a non-analytic version of the tableau system.
Modal Logic; Temporal Logic; Combination of Logics
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/11562/435197
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact