Lógicas modais axiomatizadas com profundidade de aninhamento uma que é improvável que esteja no PSPACE?

12

Estou procurando lógicas modais, axiomatizadas por um conjunto finito de axiomas de profundidade de aninhamento modal um e cujo problema de satisfação / derivabilidade dificilmente estará no PSPACE. Sem a restrição na profundidade de aninhamento modal, isso não é um problema, consulte, por exemplo, PDL. Mas parece que, ao provar, por exemplo, dureza EXPTIME por redução a algum tipo de problema de ladrilho ou de aceitação para máquinas de Turing, seria necessário algum tipo de transitividade, axiomatizada na profundidade dois. Também existem lógicas indecidíveis com uma modalidade binária (Kurucz et al .: Lógicas decidíveis e indecidíveis com uma modalidade binária , 1995), mas essas tipicamente requerem associatividade, que também é de profundidade dois. Na Lógica Condicional, novamente parece que precisamos da profundidade dois para a dureza EXPTIME (Friedman, Halpern:Sobre a complexidade das lógicas condicionais , 1994).

Podemos obter dureza EXPTIME com axiomas de profundidade de aninhamento um?

Antecedentes: Estamos tentando encontrar procedimentos de decisão genéricos de boa complexidade para lógicas axiomatisizadas com profundidade de aninhamento um.

Bjoern Lellmann
fonte

Respostas:

4

Acabei de perceber que existe uma boa solução para o seu problema, se você estiver disposto a considerar a lógica linear como sua lógica ambiental, em vez de lógica intuicionista ou clássica. Como é sabido, a lógica linear com a modalidade exponencial não é decidível. Além disso, o exponencial é uma comonada que apresenta o axioma de duplicação , que é evidentemente um axioma da profundidade de aninhamento 2.!A!A!!A

(Cheguei a esse ponto imediatamente e fiquei preso - e é por isso que essa resposta é tão tarde.)

No entanto, acabei de perceber que, na complexidade implícita, as pessoas modificam o exponencial da lógica linear para controlar com mais precisão o uso de espaço e tempo da eliminação de cortes. Criticamente, todos os sistemas para isso eliminam o axioma da duplicação! Como resultado, você pode escolher um sistema para o qual a normalização provavelmente ultrapassará o PSPACE (por exemplo, a Lógica Afinada Elementar é tão forte quanto as máquinas de Turing limitadas elementares) e, em seguida, é improvável que a axiomatização disso esteja no PSPACE, pois isso implicaria que você pode encontrar provas sem cortes rapidamente.!A

Link: Ugo dal Lago e Simone Martini, Fase Semântica e Decidibilidade da Lógica Afetiva Elementar

Neel Krishnaswami
fonte
0

Eu sugeriria a leitura do livro de Blackburn, de Rijke e Venema, Modal Logic .

Roubar
fonte
2
Com base na maneira como a pergunta é formulada, parece bastante claro que Bjoern está bastante familiarizado com o livro.
András Salamon
Embora a leitura deste livro seja sempre uma boa ideia, não pude encontrar muita informação sobre minha pergunta. Os exemplos de dureza EXPTIME (ou indecidibilidade) fazem uso de uma axiomatização de profundidade 2 (ou mais), principalmente para uma relação de acessibilidade transitiva. Você tinha uma seção / exemplo específico em mente?
Bjoern Lellmann
1
Acho que você registrou uma nova conta com o mesmo nome e é por isso que não pode comentar. Os moderadores devem poder mesclar essas contas ..?
Neel Krishnaswami
@Bjoern, feito conforme solicitado. (O problema: parece que, como Neel disse, você criou uma nova conta enquanto usava outra conta de usuário não registrada para postar a pergunta. Mesclei suas contas para que você não tenha mais problemas em comentar (pode levar algumas horas para . base de dados do sistema para atualização) Deixe-me saber se o persiste problema).
Kaveh