Buena referencia sobre métodos aproximados para resolver problemas lógicos.

Se sabe que muchos problemas lógicos (por ejemplo, problemas de satisfacción de varias lógicas modales) no son decidibles. También hay muchos problemas indecidibles en la teoría de algoritmos, por ejemplo, en la optimización combinatoria. Pero en la práctica, los heurísticos y los algoritmos aproximados funcionan bien para los algoritmos prácticos.

Por lo tanto, uno puede esperar que los algoritmos aproximados para problemas lógicos también sean adecuados. Sin embargo, la única tendencia de investigación en este sentido que he logrado encontrar es el problema max-SAT y su desarrollo estuvo activo en los noventa.

¿Existen otras tendencias de investigación activas, talleres, palabras clave, buenas referencias para el uso y desarrollo de métodos aproximados para lógicas modales, programación lógica, etc.?

Si se espera que el razonamiento automatizado gane prominencia en las futuras aplicaciones de la informática, entonces uno tendrá que ser capaz de ir más allá de las limitaciones de indecidibilidad de la lógica y los métodos aproximados o la heurística pueden ser el camino natural a seguir, ¿no es así?

La motivación que declaras para lidiar con la indecidibilidad se aplica también a problemas decidibles pero difíciles. Si tiene un problema que es NP-hard o PSPACE-hard, normalmente tendremos que usar alguna forma de aproximación (en el sentido amplio del término) para encontrar una solución.

Es útil distinguir entre diferentes nociones de aproximación.

• $\varepsilon$
• $\delta$

$(\varepsilon,\delta)$

Aquí hay un ejemplo de una noción diferente de aproximación. Suponga que realiza un cálculo como multiplicar dos números grandes y desea verificar si la multiplicación fue correcta. Existen muchas técnicas heurísticas que se utilizan en la práctica para verificar la corrección sin repetir el cálculo nuevamente. Puede verificar que los signos se multiplicaron para obtener el signo correcto. Puede verificar si los números tienen la paridad correcta (propiedades de números pares / impares). Puede usar un cheque más sofisticado como Lanzar nueves. Todas estas técnicas tienen una propiedad común que pueden decirle si cometió un error, pero no pueden garantizarle si obtuvo la respuesta correcta. Esta propiedad se puede ver como una aproximación lógica porque es posible que pueda probar que el cálculo original es incorrecto, pero es posible que no pueda probar que es correcto.

Todos los controles que he mencionado anteriormente son ejemplos de una técnica llamada interpretación abstracta. La interpretación abstracta hace una noción completamente rigurosa de aproximación lógica distinta de las aproximaciones numéricas y probabilísticas. El problema que describí con el análisis de un solo cálculo se extiende al caso más complejo de análisis de un programa. La literatura sobre interpretación abstracta ha desarrollado técnicas y marcos para el razonamiento aproximado y lógico sobre los programas y, más recientemente, sobre la lógica. Las siguientes referencias pueden ser útiles.

1. Interpretación abstracta en una cáscara de nuez por Patrick Cousot, que es una descripción simple.
2. Descripción general de Abstracción por Patrick Cousot, como parte de su curso. Hay un muy buen ejemplo de abstracción para determinar las propiedades de un ramo de flores. La analogía del ramo incluye puntos fijos y puede hacerse completamente matemáticamente precisa.
3. Curso de interpretación abstracta de Patrick Cousot, si quieres toda la profundidad y detalles.
4. Interpretación abstracta y aplicación a programas lógicos , Patrick Cousot y Radhia Cousot, 1992. Se aplica a programas lógicos, según su solicitud. La sección inicial también formaliza el procedimiento de expulsión de nueves como una interpretación abstracta.

Todo esto se ha aplicado típicamente a la razón sobre los programas de computadora. Ha habido un trabajo bastante reciente sobre la aplicación de ideas de interpretación abstracta para estudiar los procedimientos de decisión para la lógica. El enfoque no ha sido la lógica modal, sino la satisfacción en la lógica proposicional y las teorías de primer orden libres de cuantificadores. (Como he trabajado en este espacio, uno de los siguientes trabajos es mío)

1. Una generalización del método de Staalmarck por Aditya Thakur y Thomas Reps, 2012. Da una generalización del método de Staalmarck a los problemas en el análisis de programas.
2. El producto reducido de dominios abstractos y la combinación de procedimientos de decisión , Patrick Cousot, Radhia Cousot y Laurent Mauborgne, 2011. Este artículo estudia la técnica Nelson-Oppen para combinar procedimientos de decisión y muestra que también se puede usar para combinaciones incompletas, que es particularmente interesante si tienes problemas indecidibles.
3. Los solucionadores de satisfacción son analizadores estáticos , mi trabajo con Leopold Haller y Daniel Kroening, 2012. Aplica la vista de aproximación basada en la red para caracterizar los solucionadores existentes. También podrías mirar mis diapositivas sobre el tema .

Ahora ninguno de los documentos anteriores responde a su pregunta específica sobre atacar problemas de satisfacción que son indecidibles. Lo que hacen estos trabajos es adoptar una visión orientada a la aproximación de los problemas lógicos que no sea numérica o probabilística. Esta opinión se ha aplicado ampliamente para razonar sobre los programas y creo que aborda exactamente lo que está preguntando.

Para aplicarlo a la lógica modal, sugeriría que un punto de partida es utilizar la semántica algebraica de Jonsson y Tarski o la semántica posterior de Lemmon y Scott. Esto se debe a que la interpretación abstracta se formula en términos de redes y funciones monótonas, por lo que las álgebras booleanas con operadores son una semántica conveniente para trabajar. Si desea comenzar con los marcos de Kripke, puede aplicar el teorema de dualidad de Jonsson y Tarski (que algunos pueden llamar dualidad de Stone) y derivar la representación algebraica. A partir de entonces, puede aplicar los teoremas de interpretación abstracta para aproximación lógica.