En lógica matemática , la lógica monádica de segundo orden ( MSO ) es el fragmento de la lógica de segundo orden donde la cuantificación de segundo orden se limita a la cuantificación sobre conjuntos. [1] Es particularmente importante en la lógica de grafos , debido al teorema de Courcelle , que proporciona algoritmos para evaluar fórmulas monádicas de segundo orden sobre grafos de ancho de árbol acotado . También es de importancia fundamental en la teoría de autómatas , donde el teorema de Büchi-Elgot-Trakhtenbrot proporciona una caracterización lógica de los lenguajes regulares .
La lógica de segundo orden permite la cuantificación sobre predicados . Sin embargo, la lógica de segundo orden es el fragmento en el que la cuantificación de segundo orden se limita a predicados monádicos (predicados que tienen un solo argumento). Esto se describe a menudo como cuantificación sobre "conjuntos" porque los predicados monádicos son equivalentes en poder expresivo a los conjuntos (el conjunto de elementos para los que el predicado es verdadero).
La lógica monádica de segundo orden se presenta en dos variantes. En la variante considerada sobre estructuras como grafos y en el teorema de Courcelle, la fórmula puede involucrar predicados no monádicos (en este caso el predicado de arista binaria ), pero la cuantificación está restringida a ser sobre predicados monádicos solamente. En la variante considerada en la teoría de autómatas y el teorema de Büchi–Elgot–Trakhtenbrot, todos los predicados, incluidos aquellos en la fórmula misma, deben ser monádicos, con las excepciones de las relaciones de igualdad ( ) y ordenación ( ).
La lógica monádica existencial de segundo orden (EMSO) es el fragmento de MSO en el que todos los cuantificadores sobre conjuntos deben ser cuantificadores existenciales , fuera de cualquier otra parte de la fórmula. Los cuantificadores de primer orden no están restringidos. Por analogía con el teorema de Fagin , según el cual la lógica existencial (no monádica) de segundo orden captura precisamente la complejidad descriptiva de la clase de complejidad NP , la clase de problemas que se pueden expresar en la lógica monádica existencial de segundo orden se ha llamado NP monádica. La restricción a la lógica monádica permite probar separaciones en esta lógica que permanecen sin probar para la lógica de segundo orden no monádica. Por ejemplo, en la lógica de grafos , probar si un grafo está desconectado pertenece a la NP monádica, ya que la prueba se puede representar mediante una fórmula que describe la existencia de un subconjunto propio de vértices sin aristas que los conecten con el resto del grafo; Sin embargo, el problema complementario, que prueba si un gráfico está conexo, no pertenece al NP monádico. [2] [3] La existencia de un par análogo de problemas complementarios, de los cuales solo uno tiene una fórmula existencial de segundo orden (sin la restricción a las fórmulas monádicas) es equivalente a la desigualdad de NP y coNP , una cuestión abierta en complejidad computacional.
Por el contrario, cuando deseamos verificar si una fórmula MSO booleana se satisface en un árbol finito de entrada , este problema se puede resolver en tiempo lineal en el árbol, traduciendo la fórmula MSO booleana a un autómata de árbol [4] y evaluando el autómata en el árbol. En términos de la consulta, sin embargo, la complejidad de este proceso es generalmente no elemental . [5] Gracias al teorema de Courcelle , también podemos evaluar una fórmula MSO booleana en tiempo lineal en un grafo de entrada si el ancho del árbol del grafo está limitado por una constante.
Para las fórmulas MSO que tienen variables libres , cuando los datos de entrada son un árbol o tienen un ancho de árbol acotado, existen algoritmos de enumeración eficientes para producir el conjunto de todas las soluciones, [6] asegurando que los datos de entrada se preprocesen en tiempo lineal y que cada solución se produzca luego en un retardo lineal en el tamaño de cada solución, es decir, retardo constante en el caso común donde todas las variables libres de la consulta son variables de primer orden (es decir, no representan conjuntos). También existen algoritmos eficientes para contar el número de soluciones de la fórmula MSO en ese caso. [7]
El problema de satisfacibilidad de la lógica monádica de segundo orden es indecidible en general porque esta lógica subsume la lógica de primer orden .
La teoría monádica de segundo orden del árbol binario completo infinito , denominada S2S , es decidible . [8] Como consecuencia de este resultado, las siguientes teorías son decidibles:
Para cada una de estas teorías (S2S, S1S, WS2S, WS1S), la complejidad del problema de decisión no es elemental . [5] [9]
La lógica monádica de segundo orden de los árboles tiene aplicaciones en la verificación formal . Los procedimientos de decisión para la satisfacibilidad de MSO [10] [11] [12] se han utilizado para demostrar propiedades de programas que manipulan estructuras de datos enlazadas , [13] como una forma de análisis de formas y para el razonamiento simbólico en la verificación de hardware . [14]
