Computation and Size of Interpolants for Hybrid Modal Logics

Resumen Técnico: Computación y Tamaño de Interpolantes para Lógicas Modales Híbridas

Enunciado del Problema
El artículo aborda la complejidad computacional y la construcción de interpolantes de Craig en lógicas modales híbridas (específicamente $H$, $H@$, $H@,U$, y sus extensiones graduadas $GHL$). Si bien investigaciones recientes han establecido la complejidad de decidir la existencia de interpolantes en lógicas que carecen de la Propiedad de Interpolación de Craig (PIC), la construcción de tales interpolantes sigue siendo un desafío abierto. Los procedimientos de decisión existentes son no constructivos, basándose en argumentos de compacidad (por ejemplo, la consistencia conjunta de Robinson) en lugar de proporcionar fórmulas explícitas. En consecuencia, no se conocen cotas superiores significativas sobre el tamaño de los interpolantes para estas lógicas.

Este problema es particularmente agudo para las lógicas modales híbridas (y las lógicas de descripción con nominales) porque:

1. La PIC no puede restaurarse añadiendo conectivos lógicos sin sacrificar la decidibilidad.
2. Los interpolantes en estas lógicas tienen aplicaciones críticas en la representación del conocimiento, como explicar violaciones de modularidad, separar ejemplos de datos positivos y negativos, y proporcionar descripciones definidas.

Metodología
Los autores introducen una nueva técnica constructiva llamada eliminación de hipermosaicos. Este método extiende el procedimiento estándar de "eliminación de tipos" utilizado para la satisfacibilidad en lógicas modales y el enfoque de "mosaico" utilizado para decidir la existencia de interpolantes en lógicas sin PIC.

1. De Tipos a Mosaicos a Hipermosaicos:

   • La eliminación de tipos estándar trabaja con pares de tipos.
   • La eliminación de mosaicos (utilizada en procedimientos de decisión) trabaja con pares de conjuntos de tipos para manejar nominales no compartidos.
   • Los autores argumentan que la eliminación de mosaicos es demasiado local para calcular interpolantes, ya que no puede capturar interacciones globales entre diferentes "casos nominales" (escenarios sobre cómo se interpretan los nominales).
   • Para superar esto, definen hipermosaicos: conjuntos de mosaicos que deben realizarse simultáneamente en modelos bisimilares. Esta estructura permite al algoritmo rastrear restricciones globales a través de diferentes interpretaciones nominales.

2. Procedimiento de Eliminación:

   • El procedimiento comienza con un conjunto de todos los hipermosaicos $\sigma$-consistentes y limpios de nominales.
   • Elimina iterativamente los hipermosaicos que carecen de un "testigo". Un testigo para un hipermosaico $H$ es un hipermosaico extensor $H'$ que satisface condiciones específicas de coherencia (por ejemplo, para lógicas graduadas, las restricciones cuantitativas sobre los sucesores deben cumplirse mediante funciones de conteo).
   • El procedimiento se estabiliza en un conjunto $Z^*$ de hipermosaicos realizables. Si el hipermosaico inicial que contiene las fórmulas de entrada es eliminado, las fórmulas no son conjuntamente consistentes y existe un interpolante.

3. Construcción Constructiva de Separadores:

   • El artículo construye hiperseparadores de manera inductiva junto con el proceso de eliminación.
   • Un hiperseparador consiste en una "distinción de casos" (escenarios exhaustivos para tipos nominales) y funciones que mapean tipos a fórmulas.
   • En cada ronda de eliminación, la distinción de casos se refina para capturar los "tipos estrella" (vecindades locales) de los hipermosaicos eliminados.
   • Esta construcción transforma la prueba de existencia no constructiva en un algoritmo explícito que genera el interpolante (o separador).

Contribuciones y Resultados Clave

• Cotas Superiores de Tamaño y Complejidad:
  El resultado principal (Teorema 1) establece que para cualquier lógica $L \in HL \cup GHL$, si existe un interpolante de Craig para $\phi \to \psi$, puede construirse en tiempo cuádruplemente exponencial, y el interpolante resultante tiene un tamaño de cuádruplemente exponencial respecto al tamaño de las fórmulas de entrada.

  • Nota: La prueba se basa en el hecho de que, aunque hay triplemente exponencialmente muchos hipermosaicos, el procedimiento de eliminación se estabiliza después de, como máximo, doblemente exponencialmente muchas rondas debido a la monotonía de los testigos.

• Cotas Inferiores:
  El artículo proporciona una cota inferior triplemente exponencial sobre el tamaño de los interpolantes de Craig (y doblemente exponencial para el tamaño de DAG) para lógicas con el modal universal ($H@,U$ y $G@,U$). Esto demuestra que los interpolantes en lógicas híbridas son intrínsecamente más grandes que en la lógica modal estándar (donde suelen ser exponenciales).

• Indecidibilidad de Interpolantes Uniformes:
  En un contraste marcado con las lógicas modales estándar e intuicionistas (donde los interpolantes uniformes siempre existen y a menudo son construibles), el artículo demuestra (Teorema 3) que la existencia de interpolantes uniformes es indecidible para cualquier lógica que contenga $H$ y esté contenida en la Lógica de Primer Orden (LPO). Esto se muestra mediante una reducción desde la indecidibilidad de definir órdenes lineales finitos de longitud par en LPO.

• Extensiones Graduadas:
  La metodología se extiende con éxito a las lógicas modales híbridas graduadas ($GHL$), que incluyen restricciones numéricas calificadas. Los autores adaptan la definición de testigo para incluir funciones de conteo y demuestran que la cota superior cuádruplemente exponencial también se cumple para estas lógicas.

Significado y Afirmaciones
Los autores afirman proporcionar las primeras cotas superiores elementales para la construcción de interpolantes de Craig en una familia de lógicas decidibles donde la PIC falla y no puede repararse fácilmente.

• Constructivo vs. No Constructivo: El trabajo cierra la brecha entre saber que existe un interpolante (decidibilidad) y cómo calcularlo. Los métodos anteriores eran no constructivos; este artículo proporciona un algoritmo explícito.
• Robustez: Se demuestra que el método de construcción es robusto bajo restricciones de lenguaje (por ejemplo, calcular interpolantes en un sub-lenguaje más débil) y puede adaptarse para manejar restricciones estándar como transitividad y reflexividad.
• Limitaciones: El artículo reconoce que la brecha exacta de complejidad entre la cota superior cuádruplemente exponencial y la cota inferior triplemente exponencial sigue abierta. Además, la extensión a relaciones inversas o al cálculo $\mu$ híbrido sigue siendo una pregunta abierta, ya que la existencia de interpolantes en esas extensiones específicas podría ser indecidible o requerir cotas no elementales.

En resumen, el artículo establece que, aunque los interpolantes en lógicas modales híbridas son computacionalmente costosos (cuádruplemente exponenciales), son efectivamente computables, ofreciendo una base constructiva para aplicaciones en representación del conocimiento que anteriormente dependían de pruebas de existencia no constructivas.