Estado del arte para la clase monádica?

11

La lógica monádica de primer orden, también conocida como la clase monádica del problema de decisión, es donde todos los predicados toman un argumento. Se demostró que era decidible por Ackermann, y está NEXPTIME-complete .

Sin embargo, problemas como SAT y SMT tienen algoritmos rápidos para resolverlos, a pesar de los límites teóricos.

Me pregunto, ¿hay investigaciones análogas a SAT / SMT para la lógica monádica de primer orden? ¿Cuál es el "estado del arte" en este caso, y ¿existen algoritmos que sean eficientes en la práctica, a pesar de alcanzar los límites teóricos en el peor de los casos?

reference-request lo.logic automated-theorem-proving program-verification first-order-logic jmite
fuente

Respuestas:

2

En un artículo de LICS de 1993, Bachmair, Ganzinger y Waldmann mostraron que las restricciones de conjunto son equivalentes a FOL monádico, en Restricciones de conjunto son la clase monádica . Si la memoria sirve, las restricciones establecidas son equivalentes a las gramáticas de árboles regulares, por lo que la mayoría de los algoritmos desarrollados allí también deberían ser FOL portátiles a monádicos.

No conozco bien el área, pero las restricciones establecidas y las gramáticas de árboles regulares se han utilizado ampliamente en el análisis de programas, por lo que debería haber trabajo en algoritmos prácticos para ellas.

Neel Krishnaswami
fuente
Sí ... Admito que mi interés en la clase monádica es resolver las restricciones establecidas, por lo que tenemos una especie de problema con el huevo y la gallina. La mayor parte de lo que he encontrado para establecer restricciones en el análisis de programas, como Banshee, es de clases restringidas que son más débiles que la clase monádica (es decir, no tienen negación ni proyección). Pero me podría estar perdiendo un montón.
jmite