Computation and Size of Interpolants for Hybrid Modal Logics

Resumo Técnico: Computação e Tamanho de Interpolantes para Lógicas Modais Híbridas

Declaração do Problema
O artigo aborda a complexidade computacional e a construção de interpolantes de Craig em lógicas modais híbridas (especificamente $H$, $H@$, $H@,U$ e suas extensões graduadas $GHL$). Embora pesquisas recentes tenham estabelecido a complexidade de decidir a existência de interpolantes em lógicas que carecem da Propriedade de Interpolação de Craig (CIP), a construção de tais interpolantes permanece um desafio aberto. Os procedimentos de decisão existentes são não-construtivos, baseando-se em argumentos de compacidade (por exemplo, consistência conjunta de Robinson) em vez de fornecer fórmulas explícitas. Consequentemente, não há limites superiores significativos conhecidos para o tamanho dos interpolantes nessas lógicas.

Esse problema é particularmente agudo para lógicas modais híbridas (e lógicas de descrição com nominais) porque:

1. A CIP não pode ser restaurada pela adição de conectivos lógicos sem sacrificar a decidibilidade.
2. Os interpolantes nessas lógicas têm aplicações críticas na representação do conhecimento, como explicar violações de modularidade, separar exemplos de dados positivos e negativos e fornecer descrições definidas.

Metodologia
Os autores introduzem uma nova técnica construtiva chamada eliminação de hipermosaicos. Este método estende o procedimento padrão de "eliminação de tipos" usado para satisfatibilidade em lógicas modais e a abordagem de "mosaico" usada para decidir a existência de interpolantes em lógicas sem CIP.

1. De Tipos para Mosaicos para Hipermosaicos:

   • A eliminação de tipos padrão trabalha com pares de tipos.
   • A eliminação de mosaicos (usada em procedimentos de decisão) trabalha com pares de conjuntos de tipos para lidar com nominais não compartilhados.
   • Os autores argumentam que a eliminação de mosaicos é muito local para calcular interpolantes, pois não consegue capturar interações globais entre diferentes "casos nominais" (cenários sobre como os nominais são interpretados).
   • Para superar isso, eles definem hipermosaicos: conjuntos de mosaicos que devem ser realizados simultaneamente em modelos bisimilares. Essa estrutura permite que o algoritmo rastreie restrições globais através de diferentes interpretações nominais.

2. Procedimento de Eliminação:

   • O procedimento começa com um conjunto de todos os hipermosaicos $\sigma$-consistentes e limpos de nominais.
   • Ele elimina iterativamente hipermosaicos que carecem de um "testemunho". Um testemunho para um hipermosaico $H$ é um hipermosaico estendido $H'$ que satisfaz condições específicas de coerência (por exemplo, para lógicas graduadas, restrições quantitativas sobre sucessores devem ser atendidas por meio de funções de contagem).
   • O procedimento estabiliza em um conjunto $Z^*$ de hipermosaicos realizáveis. Se o hipermosaico inicial contendo as fórmulas de entrada for eliminado, as fórmulas não são conjuntamente consistentes, e um interpolante existe.

3. Construção Construtiva de Separadores:

   • O artigo constrói hiperseparadores indutivamente junto com o processo de eliminação.
   • Um hiperseparador consiste em uma "distinção de casos" (cenários exaustivos para tipos nominais) e funções mapeando tipos para fórmulas.
   • Em cada rodada de eliminação, a distinção de casos é refinada para capturar os "tipos-estrela" (vizinhanças locais) dos hipermosaicos eliminados.
   • Essa construção transforma a prova de existência não-construtiva em um algoritmo explícito que gera o interpolante (ou separador).

Contribuições e Resultados Principais

• Limites Superiores de Tamanho e Complexidade:
  O resultado principal (Teorema 1) estabelece que, para qualquer lógica $L \in HL \cup GHL$, se um interpolante de Craig existir para $\phi \to \psi$, ele pode ser construído em tempo quádruplo exponencial, e o interpolante resultante terá um tamanho quádruplo exponencial em relação ao tamanho das fórmulas de entrada.

  • Nota: A prova baseia-se no fato de que, embora existam hipermosaicos triplamente exponenciais, o procedimento de eliminação estabiliza após no máximo um número duplamente exponencial de rodadas devido à monotonicidade dos testemunhos.

• Limites Inferiores:
  O artigo fornece um limite inferior triplamente exponencial para o tamanho dos interpolantes de Craig (e duplamente exponencial para o tamanho em DAG) para lógicas com o modais universal ($H@,U$ e $G@,U$). Isso demonstra que os interpolantes em lógicas híbridas são inerentemente maiores do que na lógica modal padrão (onde são tipicamente exponenciais).

• Indecidibilidade de Interpolantes Uniformes:
  Em um contraste marcante com as lógicas modais e intuicionistas padrão (onde interpolantes uniformes sempre existem e são frequentemente construtíveis), o artigo prova (Teorema 3) que a existência de interpolantes uniformes é indecidível para qualquer lógica contendo $H$ e contida na Lógica de Primeira Ordem (FO). Isso é demonstrado por meio de uma redução da indecidibilidade da definição de ordens lineares finitas de comprimento par em FO.

• Extensões Graduadas:
  A metodologia é estendida com sucesso para lógicas híbridas graduadas ($GHL$), que incluem restrições numéricas qualificadas. Os autores adaptam a definição de testemunho para incluir funções de contagem e mostram que o limite superior quádruplo exponencial também se aplica a essas lógicas.

Significância e Alegações
Os autores afirmam fornecer os primeiros limites superiores elementares para a construção de interpolantes de Craig em uma família de lógicas decidíveis onde a CIP falha e não pode ser facilmente reparada.

• Construtivo vs. Não-Construtivo: O trabalho preenche a lacuna entre saber que um interpolante existe (decidibilidade) e como calculá-lo. Métodos anteriores eram não-construtivos; este artigo fornece um algoritmo explícito.
• Robustez: O método de construção é mostrado como robusto sob restrições de linguagem (por exemplo, calculando interpolantes em uma sub-linguagem mais fraca) e pode ser adaptado para lidar com restrições padrão como transitividade e reflexividade.
• Limitações: O artigo reconhece que a lacuna exata de complexidade entre o limite superior quádruplo exponencial e o limite inferior triplo exponencial permanece aberta. Além disso, a extensão para relações inversas ou para o cálculo $\mu$ híbrido permanece uma questão em aberto, pois a existência de interpolantes nessas extensões específicas pode ser indecidível ou exigir limites não-elementares.

Em resumo, o artigo estabelece que, embora os interpolantes em lógicas modais híbridas sejam computacionalmente caros (quádruplo exponencial), eles são efetivamente computáveis, oferecendo uma base construtiva para aplicações em representação do conhecimento que anteriormente dependiam de provas de existência não-construtivas.