Computing Witnesses Using the SCAN Algorithm

Aquí se presenta un resumen técnico detallado del artículo "Computing Witnesses Using the SCAN Algorithm" de Fabian Achammer, Stefan Hetzl y Renate A. Schmidt.

1. Planteamiento del Problema

El artículo aborda la Eliminación de Cuantificadores de Segundo Orden (SOQE), el problema de encontrar una fórmula de primer orden $\psi$ lógicamente equivalente para una fórmula de segundo orden dada $\exists X \phi$ (donde $\phi$ es de primer orden). Aunque la SOQE es indecidible en general, existen algoritmos prácticos para subclases específicas.

Los autores introducen un problema más general llamado Eliminación de Cuantificadores de Segundo Orden Testificada (WSOQE). En lugar de solo encontrar una fórmula de primer orden equivalente, el objetivo es encontrar un testigo: una tupla de predicados de primer orden $\alpha$ tal que:
$$\exists X \phi \equiv \phi[X \leftarrow \alpha]$$
Esto significa que la fórmula de segundo orden es equivalente a la fórmula de primer orden obtenida sustituyendo las variables de predicado $X$ por definiciones específicas de primer orden $\alpha$.

Significado de la WSOQE:

• Cierra la brecha entre la SOQE y las Ecuaciones de Fórmulas (FEQ) (encontrar $\alpha$ tal que $\models \phi[X \leftarrow \alpha]$).
• Es crucial para aplicaciones en representación del conocimiento (olvido/proyección), teoría de la correspondencia modal y verificación de programas (encontrar invariantes de bucle).
• A diferencia de la SOQE estándar, que solo produce el resultado, la WSOQE proporciona la definición de los predicados eliminados, preservando la estructura de la base de conocimientos.

2. Metodología: El Algoritmo WSCAN

Los autores proponen WSCAN, una extensión del algoritmo SCAN existente (un demostrador de teoremas basado en saturación para SOQE). La metodología central involucra dos fases principales:

A. La Derivación SCAN

El algoritmo opera sobre conjuntos de cláusulas. Transforma la fórmula de entrada en forma normal clausal y realiza un proceso de saturación utilizando un cálculo de inferencia específico $\mathcal{I}$:

1. Resolución con Restricciones y Factorización: En lugar de la unificación estándar, estas reglas introducen restricciones de desigualdad (por ejemplo, $t \not\simeq t'$) entre términos.
2. Eliminación de Restricciones: Unifica términos para eliminar restricciones.
3. Reglas de Borrado:
   • Borrado de Pureza Extendido: Elimina cláusulas que contienen $X$ si $X$ aparece solo con una polaridad (todas positivas o todas negativas).
   • Borrado de Cláusula Purificada: Elimina una cláusula $P$ que contiene $X$ si se han realizado "suficientemente muchas" inferencias de tal manera que el conjunto de cláusulas restante implica lógicamente el cierre por resolución de $P$. Esto se formaliza mediante un criterio de redundancia hacia adelante que involucra la eliminación de variables y la subsumción.

El proceso continúa hasta que todos los literales $X$ son eliminados, resultando en un conjunto de cláusulas de primer orden $N^*$ equivalente a $\exists X N$.

B. Construcción del Testigo (De Abajo hacia Arriba)

La contribución novedosa es la extracción de un testigo $\sigma$ del historial de la derivación. El algoritmo construye el testigo hacia atrás (desde el estado final hasta el estado inicial):

1. Caso Base: Si el conjunto de cláusulas final $N_m$ no contiene $X$, la sustitución identidad es un testigo.
2. Paso Inductivo: Para cada paso de derivación $S_i$ que transforma $N_{i-1}$ en $N_i$, el algoritmo calcula una sustitución $\tau_{S_i}$ tal que si $\sigma_i$ es un testigo para $N_i$, entonces $\tau_{S_i}\sigma_i$ es un testigo para $N_{i-1}$.
   • Para pasos de inferencia estándar (Resolución, Factorización, etc.), $\tau$ es la identidad.
   • Para el Borrado de Pureza Extendido, $\tau$ establece $X$ en $\top$ o $\bot$ dependiendo de la polaridad.
   • Para el Borrado de Cláusula Purificada (el caso complejo), el algoritmo construye un testigo basado en el cierre de resolución local de la cláusula eliminada.

C. Manejo de Testigos Infinitos

El cierre de resolución utilizado para las cláusulas purificadas puede ser infinito, lo que lleva a testigos infinitos (expresados como conjunciones infinitas). El artículo introduce dos soluciones:

1. Testigos de Punto Fijo: El testigo infinito se expresa como un máximo punto fijo ($gfp$) en lógica de punto fijo. Esto proporciona una representación finita de la definición potencialmente infinita.
2. Testigos de Primer Orden (Condición Acíclica): Los autores definen una condición llamada purificación $k$-acíclica. Si el "grafo de subsumción de purificación" asociado con un paso de borrado es acíclico, el testigo puede calcularse como un predicado de primer orden finito utilizando una iteración acotada del cierre de resolución.

3. Contribuciones Clave

1. Algoritmo WSCAN: Un método completo para calcular testigos para SOQE en conjuntos de cláusulas, extendiendo el algoritmo SCAN.
2. Pruebas de Corrección:
   • Prueba de que la sustitución construida $\sigma$ es un testigo válido ($\exists X N \equiv N\sigma$).
   • Una nueva prueba de corrección para el algoritmo SCAN original derivada de la lógica de construcción de testigos.
3. Garantía de Testigo de Primer Orden: Identificación de la condición de purificación acíclica, que garantiza que el testigo resultante es una fórmula de primer orden (evitando expresiones infinitas o de punto fijo).
4. Extensión del Lema de Ackermann: Los autores demuestran que su método subsume el Lema de Ackermann (un método clásico para SOQE) y lo extiende a casos donde el predicado aparece con polaridad mixta.
5. Manejo de Teorías de Fondo: El método se extiende para manejar el razonamiento de igualdad (mediante paramodulación) y teorías de fondo de primer orden, permitiéndole resolver problemas de alcanzabilidad en grafos y otros problemas de cláusulas de Horn con restricciones.
6. Implementación Prototipo: Una implementación prototipo en el paquete de software GAPT (Arquitectura General para Teoría de la Prueba) (versión 2.19.0).

4. Resultados y Evaluación

• Implementación: El prototipo fue probado en 44 ejemplos (de la literatura y personalizados).
• Rendimiento:
  • Se encontraron derivaciones SCAN para el 90.9% de los ejemplos (40/44) dentro de un tiempo de espera de 10 segundos.
  • El cálculo del testigo fue extremadamente rápido (promedio de 0.619 ms) en comparación con encontrar la derivación (promedio de 375 ms).
  • Los tamaños de los testigos fueron generalmente pequeños (promedio de 6.9 símbolos).
• Capacidades: El sistema calculó con éxito testigos de primer orden para derivaciones que anteriormente arrojaban testigos infinitos o requerían lógica de punto fijo, específicamente en casos que involucran grafos de purificación acíclicos.
• Limitaciones:
  • El método requiere que la entrada sea un conjunto de cláusulas (variables de dominio universalmente cuantificadas).
  • No puede manejar casos donde se requiere Skolemización y no puede revertirse (por ejemplo, $\exists X \exists u \exists v (X(u) \land \neg X(v))$), ya que el testigo resultante contendría constantes de Skolem no presentes en el lenguaje original.
  • El espacio de búsqueda para las derivaciones puede ser grande; la implementación actual utiliza retroceso pero no está optimizada para conjuntos de cláusulas masivos.

5. Significado

Este trabajo es significativo porque transforma el algoritmo SCAN de una herramienta que meramente elimina cuantificadores en una que sintetiza las definiciones de los predicados eliminados.

• Puente Teórico: Unifica los campos de la Eliminación de Cuantificadores de Segundo Orden (SOQE) y las Ecuaciones de Fórmulas (FEQ), mostrando que son dos caras de la misma moneda.
• Aplicación Práctica: Al proporcionar definiciones explícitas de primer orden (testigos), el método es directamente aplicable a:
  • Representación del Conocimiento: Crear interpolantes uniformes y olvidar predicados mientras se retiene la estructura lógica.
  • Verificación: Generar automáticamente invariantes de bucle para la verificación de programas (resolviendo cláusulas de Horn con restricciones).
  • Lógica Modal: Calcular axiomas de correspondencia para lógicas modales.

El artículo establece que para una amplia clase de derivaciones (aquellas con grafos de purificación acíclicos), el complejo problema de segundo orden puede reducirse a encontrar un testigo finito de primer orden, ofreciendo una nueva herramienta poderosa para el razonamiento automatizado.