Complexity of Simple Dependent Bimodal Logics - IMAG Accéder directement au contenu
Communication Dans Un Congrès Année : 2000

Complexity of Simple Dependent Bimodal Logics

Résumé

We characterize the computational complexity of simple dependent bimodal logics. We define an operator ⊕⊆  between logics that almost behaves as the standard joint operator ⊕ except that the inclusion axiom [2]p⇒[1]p is added. Many multimodal logics from the literature are of this form or contain such fragments. For the standard modal logics K,T,B,S4 and S5 we study the complexity of the satisfiability problem of the joint in the sense of ⊕⊆ . We mainly establish the PSPACE upper bounds by designing tableaux-based algorithms in which a particular attention is given to the formalization of termination and to the design of a uniform framework. Reductions into the packed guarded fragment with only two variables introduced by M. Marx are also used. E. Spaan proved that K ⊕⊆  S5 is EXPTIME-hard. We show that for ⟨L1,L2⟩∈{K,T,B}×{S4,S5}, L1⊕⊆L2 is also EXPTIME-hard.
Fichier principal
Vignette du fichier
Dem-tableaux2000.pdf (10.36 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03195235 , version 1 (10-04-2021)

Identifiants

Citer

Stéphane Demri. Complexity of Simple Dependent Bimodal Logics. International Conference, TABLEAUX 2000, St Andrews, Scotland, Roy Dyckhoff, Jul 2000, St Andrews, United Kingdom. pp.190-204, ⟨10.1007/10722086_17⟩. ⟨hal-03195235⟩

Collections

UGA IMAG CNRS
39 Consultations
18 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More