A Strategy Language for Controlled Proof Search

Resumen Técnico: Un Lenguaje de Estrategia para la Búsqueda de Pruebas Controlada

Planteamiento del Problema
En el razonamiento automatizado, la completitud estática de un cálculo lógico (la existencia de una prueba para cualquier teorema) no garantiza la completitud dinámica de un probador (la capacidad de encontrar realmente esa prueba). En lógicas semidecidibles, las reglas de inferencia pueden generar infinitos sucesores. Si una estrategia de búsqueda de pruebas emplea una exploración injusta —como un enfoque ingenuo de búsqueda en profundidad que prioriza indefinidamente una rama—, puede posponer inferencias relevantes para siempre, fallando en el descubrimiento de pruebas válidas incluso cuando estas existen. Este problema es particularmente agudo en marcos como Pgeon, que separan las reglas de inferencia de las estrategias de búsqueda de pruebas, ya que el diseño de la política de exploración se convierte en un determinante crítico del éxito.

Metodología
El artículo introduce un lenguaje de estrategia formal para Pgeon, un marco de meta-probadores que compila especificaciones declarativas de cálculos lógicos en probadores ejecutables. El cambio metodológico central consiste en modelar la búsqueda de pruebas no como una relación entre estados, sino como la enumeración de estados de prueba mediante flujos (streams).

1. Semántica Formal: Un estado de prueba ($\Sigma$) se trata como un árbol de prueba parcialmente construido. Una estrategia se define como una función $s: \Sigma \to \text{Str}(\Sigma)$, que mapea un estado a un flujo (finito o infinito) de estados sucesores. Esto hace que la no determinidad sea explícita:

   • Un flujo vacío representa el fallo.
   • Un flujo unitario representa el éxito determinista.
   • Un flujo con múltiples elementos representa la ramificación no determinista.
   • Los flujos infinitos representan reglas que pueden generar sucesores ilimitados.

2. Combinadores: El lenguaje proporciona un conjunto de operadores para componer estas estrategias, distinguiendo entre exploración sesgada (búsqueda en profundidad) y justa (entrelazada):

   • Composición Secuencial ($;$): Aplica una estrategia a los resultados de otra.
   • Elección Sesgada a la Izquierda ($\parallel$): Intenta la primera estrategia; si falla (flujo vacío), recurre a la segunda.
   • Composición Secuencial Justa ($\&;$): Entrelaza los resultados de aplicaciones secuenciales mediante diagonalización ($\triangle$), asegurando que si un resultado es alcanzable en pasos finitos, eventualmente será explorado.
   • Elección Justa ($\&|$): Entrelaza justamente los resultados de dos estrategias alternativas.
   • Repetición ($*$): Definida como un punto fijo menor utilizando la composición secuencial justa ($\mu X. \text{id} \&; (s \&; X)$), asegurando que todas las profundidades de iteración finitas sean exploradas en lugar de proceder estrictamente en profundidad.

3. Operaciones Primitivas: El lenguaje incluye reglas primitivas ($r$) y un operador de aplicación exhaustiva ($r!$) que aplica una regla a todas las coincidencias admisibles en un estado.

Contribuciones Clave

• Semántica de Flujos Composicional: El artículo proporciona una álgebra composicional para los combinadores de estrategia donde el espacio de búsqueda se reifica como un objeto de primera clase (un flujo). Esto permite razonar sobre la justicia y la enumeración independientemente de los detalles de implementación como la disciplina de pila o las continuaciones.
• Mecanismos de Justicia (Fairness): Al introducir operadores de entrelazado basados en la diagonalización ($\&;$ y $\&|$), el marco aborda el problema de la "inanición" (starvation) donde las ramas infinitas impiden el descubrimiento de pruebas finitas.
• Lenguaje de Estrategia Formal para Pgeon: El trabajo formaliza el componente de estrategia del marco Pgeon, abstrayendo el flujo de control de la búsqueda de pruebas en un lenguaje declarativo.

Resultados y Casos de Estudio
El artículo demuestra la expresividad y efectividad del enfoque a través de dos casos de estudio:

1. Lógica de Primer Orden (LK): Los autores abordan la interacción entre el cierre (closure/unification) y la saturación de reglas. Una estrategia ingenua de aplicación repetida de reglas a menudo falla al encontrar pruebas porque se compromete con instanciaciones específicas demasiado pronto. La estrategia propuesta, $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$, utiliza la composición justa para entrelazar los intentos de cierre con la saturación de reglas. Esto asegura que diferentes elecciones de unificación sean exploradas a través de todas las profundidades de búsqueda, evitando que el sistema se quede atrapado en bucles de instanciación infinita mientras pierde una derivación de cierre.

2. Lógica Modal (S4): En S4, la regla no determinista $\theta$ (eliminación arbitraria de fórmulas) es necesaria para permitir la aplicación de la regla modal S4, pero conlleva el riesgo de descartar fórmulas necesarias para el cierre. El uso incontrolado de $\theta$ conduce a callejones sin salida. Los autores proponen una estrategia combinada $\theta^* \&; \text{S4}$, que explora todas las formas de eliminar fórmulas para permitir las aplicaciones de S4 de manera justa. Esto se integra en una estrategia mayor $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$, asegurando que si una aplicación exitosa de S4 requiere un subconjunto específico de fórmulas eliminadas, dicha configuración sea alcanzada eventualmente sin inanición.

Significancia
El artículo afirma que este enfoque ofrece una base de principios y modular para especificar y analizar procedimientos de búsqueda de pruebas. Al separar las reglas de inferencia de las estrategias de búsqueda y proporcionar un lenguaje formal con semántica composicional, el marco permite la exploración sistemática de espacios de búsqueda en lógicas semidecidibles. Demuestra que la completitud dinámica puede lograrse incluso cuando las estrategias ingenuas de búsqueda en profundidad fallan, mediante la gestión explícita de la justicia a través del entrelazado de flujos. El trabajo permite razonar sobre los procedimientos de búsqueda de pruebas a un nivel abstracto, independiente de la implementación específica del probador.