Modal logic is a paradigm for several useful and applicable formal systems in computer science, and, in particular, for temporal logics of various kinds. It generally retains the low complexity of classical propositional logic, but notable exceptions exist that present higher complexity or are even undecidable. In search of computationally well-behaved fragments, clausal forms and other sub-propositional restrictions of temporal and description logics have been recently studied. It is known that the Horn fragments of the modal logics between K and S4 are PSPACE-complete, keeping the same complexity of the the full propositional versions. In this paper, inspired by similar results in the temporal case, we sharpen the above result by showing that if we allow only box modalities in the language the Horn fragments of the modal logics between K and S4 become P-complete. Exploring the innermost reasons for the tractability of sub-Horn modal logics is a necessary condition to understand the behaviour of more expressive temporal and spatial languages under similar restrictions.

On the Complexity of Fragments of Horn Modal Logics

SCIAVICCO, Guido
2016

Abstract

Modal logic is a paradigm for several useful and applicable formal systems in computer science, and, in particular, for temporal logics of various kinds. It generally retains the low complexity of classical propositional logic, but notable exceptions exist that present higher complexity or are even undecidable. In search of computationally well-behaved fragments, clausal forms and other sub-propositional restrictions of temporal and description logics have been recently studied. It is known that the Horn fragments of the modal logics between K and S4 are PSPACE-complete, keeping the same complexity of the the full propositional versions. In this paper, inspired by similar results in the temporal case, we sharpen the above result by showing that if we allow only box modalities in the language the Horn fragments of the modal logics between K and S4 become P-complete. Exploring the innermost reasons for the tractability of sub-Horn modal logics is a necessary condition to understand the behaviour of more expressive temporal and spatial languages under similar restrictions.
2016
9781509038251
Modal Logic, Polynomial Complexity, Satisfiability Checking
File in questo prodotto:
File Dimensione Formato  
time16new.pdf

solo gestori archivio

Descrizione: Articolo
Tipologia: Full text (versione editoriale)
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 307.85 kB
Formato Adobe PDF
307.85 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in SFERA 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/11392/2353733
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact