Logiques modales axiomatisées avec une profondeur de nidification peu probable dans PSPACE?

Je recherche des logiques modales, axiomatisées par un ensemble fini d'axiomes de profondeur de nidification modale un, et dont le problème de satisfiabilité / dérivabilité est peu probable dans PSPACE. Sans la restriction de la profondeur d'imbrication modale, ce n'est pas un problème, voir par exemple PDL. Mais il semble qu'en prouvant par exemple la dureté EXPTIME par réduction à une sorte de problème de carrelage ou de problème d'acceptation pour les machines de Turing, il faudrait une sorte de transitivité, qui est axiomatisée en profondeur deux. Il existe également des logiques indécidables avec une modalité binaire (Kurucz et al .: Logiques décidables et indécidables avec une modalité binaire , 1995), mais celles-ci nécessitent généralement l'associativité, qui est également la profondeur deux. Dans la logique conditionnelle, encore une fois, il semble que nous ayons besoin de la profondeur deux pour la dureté EXPTIME (Friedman, Halpern:Sur la complexité des logiques conditionnelles , 1994).

Peut-on obtenir une dureté EXPTIME avec des axiomes de profondeur de nidification un?

Contexte: Nous essayons de trouver des procédures de décision génériques d'une bonne complexité pour les logiques axiomatisées avec une profondeur d'imbrication une.

Je viens de réaliser qu'il existe une bonne solution à votre problème, si vous êtes prêt à considérer la logique linéaire comme votre logique ambiante au lieu de la logique intuitionniste ou classique. Comme cela est bien connu, la logique linéaire avec la modalité exponentielle n'est pas décidable. De plus, l'exponentielle est une comonade comportant l'axiome de duplication , qui est évidemment un axiome de profondeur d'imbrication 2.$!A$$!A \multimap !!A$

(Je suis arrivé si loin tout de suite, puis je suis resté coincé - c'est pourquoi cette réponse est si tardive.)

Cependant, je viens de réaliser que dans la complexité implicite, les gens modifient l'exponentielle de la logique linéaire pour contrôler plus précisément l'utilisation de l'espace et du temps de l'élimination des coupures. De manière critique, tous les systèmes pour ce faire éliminent l'axiome de duplication! Par conséquent, vous pouvez choisir un système pour lequel la normalisation va probablement au-delà de PSPACE (par exemple, la logique affine élémentaire est aussi forte que les machines de Turing bornées élémentaires), puis l'axiomatisation de celui-ci ne sera probablement pas dans PSPACE, car cela impliquerait que vous pouvez trouver rapidement des épreuves sans coupure.$!A$

Lien: Ugo dal Lago et Simone Martini, Phase sémantique et décidabilité de la logique affine élémentaire

Je suggère de lire le livre Modal Logic de Blackburn, de Rijke et Venema .