Lógica de grafos

Formulación lógica de propiedades de grafos

En los campos matemáticos de la teoría de grafos y la teoría de modelos finitos , la lógica de grafos se ocupa de las especificaciones formales de las propiedades de los grafos mediante sentencias de lógica matemática . Existen varias variaciones en los tipos de operaciones lógicas que se pueden utilizar en estas sentencias. La lógica de grafos de primer orden se refiere a sentencias en las que las variables y los predicados se refieren a vértices y aristas individuales de un grafo, mientras que la lógica de grafos monádica de segundo orden permite la cuantificación sobre conjuntos de vértices o aristas. Las lógicas basadas en operadores de punto fijo mínimo permiten predicados más generales sobre tuplas de vértices, pero estos predicados solo se pueden construir mediante operadores de punto fijo, lo que restringe su poder.

Una oración puede ser verdadera para algunos grafos y falsa para otros; se dice que un grafo modela , escrito , si es verdadero para los vértices y la relación de adyacencia de . El problema algorítmico de la comprobación de modelos se refiere a comprobar si un grafo dado modela una oración dada. El problema algorítmico de la satisfacibilidad se refiere a comprobar si existe un grafo que modela una oración dada. Aunque tanto la comprobación de modelos como la satisfacibilidad son difíciles en general, varios metateoremas algorítmicos importantes muestran que las propiedades expresadas de esta manera se pueden comprobar de manera eficiente para clases importantes de grafos. ${\displaystyle S}$ ${\displaystyle G}$ ${\displaystyle S}$ ${\displaystyle G\models S}$ ${\displaystyle S}$ ${\displaystyle G}$

Otros temas de investigación en la lógica de gráficos incluyen investigaciones de la probabilidad de que un gráfico aleatorio tenga una propiedad especificada dentro de un tipo particular de lógica y métodos de compresión de datos basados ​​en la búsqueda de oraciones lógicas que estén modeladas por un gráfico único.

Primer orden

El gráfico que se muestra aquí aparece como un subgráfico de un gráfico no dirigido si y solo si modela la oración . ${\displaystyle G}$ ${\displaystyle G}$ ${\displaystyle \exists x_{1},x_{2},x_{3},x_{4}.}$ ${\displaystyle x_{1}\sim x_{2}}$ ${\displaystyle \land }$ ${\displaystyle x_{2}\sim x_{3}}$ ${\displaystyle \land }$ ${\displaystyle x_{3}\sim x_{1}}$ ${\displaystyle \land }$ ${\displaystyle x_{3}\sim x_{4}}$ ${\displaystyle \land }$ ${\displaystyle x_{1}\neq x_{4}}$ ${\displaystyle \land }$ ${\displaystyle x_{2}\neq x_{4}}$

En la lógica de primer orden de los gráficos, una propiedad de un gráfico se expresa como una oración lógica cuantificada cuyas variables representan los vértices del gráfico , con predicados para pruebas de igualdad y adyacencia. ^[1]

Ejemplos

Por ejemplo, la condición de que un grafo no tenga ningún vértice aislado puede expresarse mediante la oración donde el símbolo indica la relación de adyacencia no dirigida entre dos vértices. Esta oración puede interpretarse como que para cada vértice hay otro vértice adyacente a . ^[1] $${\displaystyle \forall u\exists v(u\sim v)}$$ ${\displaystyle \sim }$ ${\displaystyle u}$ ${\displaystyle v}$ ${\displaystyle u}$

El problema de isomorfismo de subgrafos para un subgrafo fijo pregunta si aparece como un subgrafo de un grafo más grande . Puede expresarse mediante una oración que establezca la existencia de vértices (uno para cada vértice de ) tales que, para cada arista de , el par correspondiente de variables represente vértices adyacentes y tales que, para cada par restante de vértices de , el par correspondiente de variables represente vértices distintos; ^[2] vea la ilustración. Como caso especial, el problema de la camarilla (para un tamaño de camarilla fijo) puede expresarse mediante una oración que establezca la existencia de un número de vértices igual al tamaño de la camarilla, todos los cuales son adyacentes. ^[3] ${\displaystyle H}$ ${\displaystyle H}$ ${\displaystyle G}$ ${\displaystyle H}$ ${\displaystyle H}$ ${\displaystyle H}$

Axiomas

Para gráficos simples no dirigidos , la teoría de gráficos de primer orden incluye los axiomas

${\displaystyle \forall u{\bigl (}\lnot (u\sim u){\bigr )}}$(el gráfico no puede contener ningún bucle ), y

${\displaystyle \forall u\forall v(u\sim v\Rightarrow v\sim u)}$(los bordes no están dirigidos). ^[4]

Otros tipos de gráficos, como los gráficos dirigidos , pueden involucrar diferentes axiomas, ^[5] y las formulaciones lógicas de propiedades multigráficas requieren un manejo especial, como tener múltiples relaciones de aristas ^[6] o variables separadas para vértices y aristas. ^[7]

Ley del cero-uno

El gráfico de Rado , un gráfico infinito que modela exactamente las oraciones de primer orden que casi siempre son verdaderas de los gráficos finitos.

Glebskiĭ et al. (1969) e, independientemente, Fagin (1976) demostraron una ley cero-uno para la lógica de grafos de primer orden; la prueba de Fagin utilizó el teorema de compacidad . Según este resultado, cada oración de primer orden es casi siempre verdadera o casi siempre falsa para grafos aleatorios en el modelo de Erdős–Rényi . Es decir, sea una oración fija de primer orden y elija un grafo de vértice aleatorio de manera uniforme al azar entre todos los grafos en un conjunto de vértices etiquetados. Entonces, en el límite como tiende a infinito, la probabilidad de que los modelos tiendan a cero o a uno: Además, hay un grafo infinito específico, el grafo de Rado , tal que las oraciones modeladas por el grafo de Rado son exactamente aquellas para las cuales la probabilidad de ser modeladas por un grafo finito aleatorio tiende a uno: Para grafos aleatorios en los que cada arista se incluye independientemente de las otras con una probabilidad fija, el mismo resultado es verdadero, con las mismas oraciones que tienen probabilidades que tienden a cero o a uno. ^[8] ${\displaystyle S}$ ${\displaystyle n}$ ${\displaystyle G_{n}}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle G_{n}}$ ${\displaystyle S}$ $${\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}$$ ${\displaystyle R}$ $${\displaystyle R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]=1.}$$

La complejidad computacional de determinar si una oración dada tiene una probabilidad que tiende a cero o a uno es alta: el problema es PSPACE-completo . ^[9] Si una propiedad de un gráfico de primer orden tiene una probabilidad que tiende a uno en gráficos aleatorios, entonces es posible enumerar todos los gráficos de vértice que modelan la propiedad, con un retraso polinomial (como una función de ) por gráfico. ^[4] ${\displaystyle n}$ ${\displaystyle n}$

Se puede realizar un análisis similar para grafos aleatorios no uniformes, donde la probabilidad de incluir una arista es una función del número de vértices, y donde la decisión de incluir o excluir una arista se toma independientemente con igual probabilidad para todas las aristas. Sin embargo, para estos grafos la situación es más complicada. En este caso, una propiedad de primer orden puede tener uno o más umbrales, de modo que cuando la probabilidad de inclusión de una arista está acotada lejos del umbral, entonces la probabilidad de tener la propiedad dada tiende a cero o uno. Estos umbrales nunca pueden ser una potencia irracional de , por lo que los grafos aleatorios donde la probabilidad de inclusión de una arista es una potencia irracional obedecen una ley cero-uno análoga a la de los grafos uniformemente aleatorios. Una ley cero-uno similar se cumple para grafos aleatorios muy dispersos que tienen una probabilidad de inclusión de una arista de con , siempre que no sea una razón superparticular . ^[10] Si es superparticular, la probabilidad de tener una propiedad dada puede tender a un límite que no es cero o uno, pero este límite se puede calcular de manera eficiente. ^[11] Existen oraciones de primer orden que tienen infinitos umbrales. ^[12] ${\displaystyle n}$ ${\displaystyle n^{-c}}$ ${\displaystyle c>1}$ ${\displaystyle c}$ ${\displaystyle c}$

Complejidad parametrizada

Si una oración de primer orden incluye variables distintas, entonces la propiedad que describe puede probarse en gráficos de vértices examinando todas las -tuplas de vértices; sin embargo, este algoritmo de búsqueda de fuerza bruta no es particularmente eficiente, ya que lleva tiempo . El problema de verificar si un gráfico modela una oración de primer orden dada incluye como casos especiales el problema de isomorfismo de subgrafos (en el que la oración describe los gráficos que contienen un subgrafo fijo) y el problema de la camarilla (en el que la oración describe gráficos que contienen subgrafos completos de un tamaño fijo). El problema de la camarilla es difícil para W(1) , el primer nivel de una jerarquía de problemas difíciles desde el punto de vista de la complejidad parametrizada . Por lo tanto, es poco probable tener un algoritmo manejable con parámetros fijos, uno cuyo tiempo de ejecución tome la forma de una función y una constante que sean independientes de y . ^[13] Más fuertemente, si la hipótesis del tiempo exponencial es verdadera, entonces la búsqueda de camarillas y la verificación del modelo de primer orden necesariamente tomarían un tiempo proporcional a una potencia de cuyo exponente es proporcional a . ^[14] ${\displaystyle k}$ ${\displaystyle n}$ ${\displaystyle k}$ ${\displaystyle O(n^{k})}$ ${\displaystyle O(f(k)n^{c})}$ ${\displaystyle f}$ ${\displaystyle c}$ ${\displaystyle k}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle k}$

En clases restringidas de grafos, la comprobación de modelos de oraciones de primer orden puede ser mucho más eficiente. En particular, cada propiedad de grafo expresable como una oración de primer orden puede ser comprobada en tiempo lineal para los grafos de expansión acotada . Estos son los grafos en los que todos los menores superficiales son grafos dispersos , con una relación de aristas a vértices acotada por una función de la profundidad del menor. Incluso de manera más general, la comprobación de modelos de primer orden puede realizarse en tiempo casi lineal para grafos densos en ninguna parte, clases de grafos para los cuales, en cada profundidad posible, hay al menos un menor superficial prohibido. Por el contrario, si la comprobación de modelos es manejable con parámetros fijos para cualquier familia monótona de grafos, esa familia debe ser densa en ninguna parte. ^[15]

Compresión de datos e isomorfismo de grafos

Se dice que una oración de primer orden en la lógica de grafos define un grafo si es el único grafo que modela . Cada grafo puede definirse mediante al menos una oración; por ejemplo, se puede definir cualquier grafo de -vértice mediante una oración con variables, una para cada vértice del grafo y una más para indicar la condición de que no haya ningún vértice distinto de los vértices del grafo. Se pueden usar cláusulas adicionales de la oración para garantizar que no haya dos variables de vértice iguales, que cada borde de esté presente y que no exista ningún borde entre un par de vértices no adyacentes de . Sin embargo, para algunos grafos existen oraciones significativamente más cortas que definen el grafo. ^[16] ${\displaystyle S}$ ${\displaystyle G}$ ${\displaystyle G}$ ${\displaystyle S}$ ${\displaystyle n}$ ${\displaystyle G}$ ${\displaystyle n+1}$ ${\displaystyle n}$ ${\displaystyle G}$ ${\displaystyle G}$

Se pueden definir varios invariantes de grafos diferentes a partir de las oraciones más simples (con diferentes medidas de simplicidad) que definen un grafo dado. En particular, la profundidad lógica de un grafo se define como el nivel mínimo de anidamiento de cuantificadores (el rango de cuantificador ) en una oración que define el grafo. ^[17] La ​​oración descrita anteriormente anida los cuantificadores para todas sus variables, por lo que tiene una profundidad lógica . El ancho lógico de un grafo es el número mínimo de variables en una oración que lo define. ^[17] En la oración descrita anteriormente, este número de variables es nuevamente . Tanto la profundidad lógica como el ancho lógico se pueden acotar en términos del ancho de árbol del grafo dado. ^[18] La longitud lógica, análogamente, se define como la longitud de la oración más corta que describe el grafo. La oración descrita anteriormente tiene una longitud proporcional al cuadrado del número de vértices, pero es posible definir cualquier grafo mediante una oración con una longitud proporcional a su número de aristas. ^[17] ${\displaystyle n+1}$ ${\displaystyle n+1}$

Todos los árboles, y la mayoría de los grafos, pueden describirse mediante oraciones de primer orden con solo dos variables, pero extendidas mediante predicados de conteo. Para los grafos que pueden describirse mediante oraciones en esta lógica con un número constante fijo de variables, es posible encontrar una canonización de grafos en tiempo polinomial (con el exponente del polinomio igual al número de variables). Al comparar canonizaciones, es posible resolver el problema de isomorfismo de grafos para estos grafos en tiempo polinomial. ^[19]

Satisfacción

Como caso especial del teorema de Trakhtenbrot , es indecidible si una oración de primer orden dada puede ser realizada por un grafo finito no dirigido. Esto significa que ningún algoritmo puede responder correctamente a esta pregunta para todas las oraciones. ^[20]

Algunas oraciones de primer orden se modelan mediante grafos infinitos, pero no mediante ningún grafo finito. Por ejemplo, la propiedad de tener exactamente un vértice de grado uno, y todos los demás vértices de grado exactamente dos, se puede expresar mediante una oración de primer orden. Se modela mediante un rayo infinito, pero viola el lema de Euler para grafos finitos. Sin embargo, de la solución negativa al Entscheidungsproblem (de Alonzo Church y Alan Turing en la década de 1930) se deduce que la satisfacibilidad de las oraciones de primer orden para grafos que no están restringidos a ser finitos sigue siendo indecidible. También es indecidible distinguir entre las oraciones de primer orden que son verdaderas para todos los grafos y las que son verdaderas para grafos finitos pero falsas para algunos grafos infinitos. ^[21]

Punto fijo

Se define un vértice como débil (resaltado en rojo) si, con una sola excepción como máximo , cada uno de sus vecinos es débil, según la fórmula de punto fijo . Los vértices azules restantes forman el núcleo 2 del grafo. ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle W(x)\leftarrow \exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee W(z)){\bigr )}}$

Las lógicas de grafos basadas en el punto mínimo fijo extienden la lógica de primer orden de los grafos al permitir predicados (propiedades de vértices o tuplas de vértices) definidos por operadores especiales de punto fijo. Este tipo de definición comienza con una implicación, una fórmula que establece que cuando ciertos valores del predicado son verdaderos, entonces otros valores también lo son. Un "punto fijo" es cualquier predicado para el cual esta es una implicación válida. Puede haber muchos puntos fijos, incluido el predicado siempre verdadero; un "punto mínimo fijo" es un punto fijo que tiene la menor cantidad posible de valores verdaderos. Más precisamente, sus valores verdaderos deberían ser un subconjunto de los valores verdaderos de cualquier otro punto fijo. ^[22]

Por ejemplo, definamos que es verdadero cuando los dos vértices y están conectados por un camino en un grafo dado, y falso en caso contrario. Entonces cada vértice está conectado a sí mismo, y cuando está conectado a un vecino de , también está conectado por un paso más a . Expresando este razonamiento en términos lógicos, es el punto menos fijo de la fórmula Aquí, ser un punto fijo significa que la verdad del lado derecho de la fórmula implica la verdad del lado izquierdo, como sugiere la flecha de implicación invertida. Ser el punto menos fijo, en este caso, implica que no se definirán dos vértices como conectados a menos que su conectividad provenga del uso repetido de esta implicación. ^[22] ${\displaystyle C(u,v)}$ ${\displaystyle u}$ ${\displaystyle v}$ ${\displaystyle u}$ ${\displaystyle v}$ ${\displaystyle v}$ ${\displaystyle C}$ $${\displaystyle C(u,v)\leftarrow {\Bigl (}(u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.}$$

Se han estudiado varias variaciones de la lógica de punto fijo. En la lógica de punto fijo mínimo, el lado derecho del operador en la fórmula definitoria debe usar el predicado solo de manera positiva (es decir, cada aparición debe estar anidada dentro de un número par de negaciones) para que el punto fijo mínimo esté bien definido. En otra variante con poder lógico equivalente, la lógica de punto fijo inflacionario, la fórmula no necesita ser monótona, sino que el punto fijo resultante se define como el que se obtiene al aplicar repetidamente las implicaciones derivadas de la fórmula definitoria a partir del predicado completamente falso. También son posibles otras variantes, que permiten implicaciones negativas o predicados múltiples definidos simultáneamente, pero no brindan poder de definición adicional. Un predicado, definido de una de estas maneras, puede entonces aplicarse a una tupla de vértices como parte de una oración lógica más grande. ^[22] ${\displaystyle \leftarrow }$

Las lógicas de punto fijo, y las extensiones de estas lógicas que también permiten contar variables enteras cuyos valores van desde 0 hasta el número de vértices, se han utilizado en complejidad descriptiva en un intento de proporcionar una descripción lógica de los problemas de decisión en la teoría de grafos que se pueden decidir en tiempo polinomial . El punto fijo de una fórmula lógica se puede construir en tiempo polinomial, mediante un algoritmo que agrega repetidamente tuplas al conjunto de valores para los cuales el predicado es verdadero hasta llegar a un punto fijo, por lo que decidir si un grafo modela una oración en esta lógica siempre se puede decidir en tiempo polinomial. No todas las propiedades de grafos en tiempo polinomial se pueden modelar mediante una oración en una lógica que solo usa puntos fijos y conteo. ^{[23] [24]} Sin embargo, para algunas clases especiales de grafos, las propiedades en tiempo polinomial son las mismas que las propiedades expresables en la lógica de punto fijo con conteo. Estos incluyen gráficos aleatorios, ^{[23] [25]} gráficos de intervalo , ^{[23] [26]} y (a través de una expresión lógica del teorema de estructura de gráficos ) cada clase de gráficos caracterizados por menores prohibidos . ^[23]

Segundo orden

En la lógica monádica de segundo orden de los grafos, las variables representan objetos de hasta cuatro tipos: vértices, aristas, conjuntos de vértices y conjuntos de aristas. Existen dos variantes principales de la lógica monádica de grafos de segundo orden: MSO _1, en la que solo se permiten variables de vértice y de conjunto de vértices, y MSO ₂ , en la que se permiten los cuatro tipos de variables. Los predicados sobre estas variables incluyen pruebas de igualdad, pruebas de pertenencia e incidencia vértice-arista (si se permiten variables de vértice y arista) o adyacencia entre pares de vértices (si solo se permiten variables de vértice). Otras variantes en la definición permiten predicados adicionales, como predicados de conteo modular. ^[27]

Ejemplos

Como ejemplo, la conectividad de un grafo no dirigido puede expresarse en MSO ₁ como la afirmación de que, para cada partición de los vértices en dos subconjuntos no vacíos, existe una arista de un subconjunto al otro. Una partición de los vértices puede describirse por el subconjunto de vértices en un lado de la partición, y cada uno de esos subconjuntos debe describir una partición trivial (una en la que uno u otro lado está vacío) o ser atravesado por una arista. Es decir, un grafo es conexo cuando modela la oración MSO _1. Sin embargo, la conectividad no puede expresarse en lógica de grafos de primer orden, ni puede expresarse en MSO ₁ existencial (el fragmento de MSO ₁ en el que todos los cuantificadores de conjuntos son existenciales y aparecen al principio de la oración) ni siquiera en MSO ₂ existencial . ^[28] ${\displaystyle S}$ $${\displaystyle \forall S{\Bigl (}\forall x(x\in S)\vee \forall y{\bigl (}\lnot (y\in S){\bigr )}\vee \exists x\exists y{\bigl (}x\in S\wedge \lnot (y\in S)\wedge x\sim y{\bigr )}{\Bigr )}.}$$

La hamiltonicidad se puede expresar en MSO ₂ por la existencia de un conjunto de aristas que forman un grafo 2-regular conectado en todos los vértices, con conectividad expresada como arriba y 2-regularidad expresada como la incidencia de dos pero no tres aristas distintas en cada vértice. Sin embargo, la hamiltonicidad no se puede expresar en MSO ₁ , porque MSO ₁ no es capaz de distinguir grafos bipartitos completos con igual número de vértices en cada lado de la bipartición (que son hamiltonianos) de grafos bipartitos completos no balanceados (que no lo son). ^[29]

Aunque no forman parte de la definición de MSO ₂ , las orientaciones de grafos no dirigidos se pueden representar mediante una técnica que implica árboles de Trémaux . Esto permite que también se expresen otras propiedades de grafos que implican orientaciones. ^[30]

Teorema de Courcelle

Según el teorema de Courcelle , cada propiedad fija MSO ₂ puede probarse en tiempo lineal en gráficos de ancho de árbol acotado , y cada propiedad fija MSO ₁ puede probarse en tiempo lineal en gráficos de ancho de camarilla acotado . ^[31] La versión de este resultado para gráficos de ancho de árbol acotado también puede implementarse en el espacio logarítmico . ^[32] Las aplicaciones de este resultado incluyen un algoritmo manejable con parámetros fijos para calcular el número de cruces de un gráfico. ^[33]

Teorema de Seese

El problema de satisfacibilidad para una oración de lógica monádica de segundo orden es el problema de determinar si existe al menos un grafo (posiblemente dentro de una familia restringida de grafos) para el cual la oración es verdadera. Para familias de grafos arbitrarias y oraciones arbitrarias, este problema es indecidible . Sin embargo, la satisfacibilidad de oraciones MSO ₂ es decidible para los grafos de ancho de árbol acotado, y la satisfacibilidad de oraciones MSO ₁ es decidible para grafos de ancho de camarilla acotado. La prueba implica usar el teorema de Courcelle para construir un autómata que pueda probar la propiedad, y luego examinar el autómata para determinar si hay algún grafo que pueda aceptar. Como recíproco parcial, ^[34] Seese (1991) demostró que, siempre que una familia de grafos tiene un problema de satisfacibilidad MSO ₂ decidible , la familia debe tener ancho de árbol acotado. La prueba se basa en un teorema de Robertson y Seymour que sostiene que las familias de grafos con un ancho de árbol ilimitado tienen menores de cuadrícula arbitrariamente grandes . Seese también conjeturó que cada familia de grafos con un problema de satisfacibilidad MSO ₁ decidible debe tener un ancho de clique acotado. ^[35] Esto no se ha demostrado, pero es cierto un debilitamiento de la conjetura que extiende MSO ₁ con predicados de conteo modular. ^[34]

Notas

1. Spencer (2001), Sección 1.2, "¿Qué es una teoría de primer orden?", págs. 15-17.
2. Verbitsky y Zhukovskii (2019).
3. Zume (2017).
4. Goldberg (1993).
5. Por ejemplo, Henson (1972) requiere que los gráficos dirigidos se describan mediante una relación asimétrica , lo que significa que no se permiten bucles ni ciclos de 2, dando como resultado gráficos orientados .
6. Koncewicz (1973).
7. Brugink y König (2018).
8. Glebskiĭ y otros (1969); Fagin (1976)
9. Grandjean (1983).
10. Shelah y Spencer (1988); Spencer (2001).
11. Linch (1992).
12. Spencer (1990).
13. Downey y Fellows (1995).
14. Chen y otros (2006).
15. Nešetřil & Ossona de Mendez (2012), 18.3 El problema del isomorfismo de subgrafos y las consultas booleanas, págs. Dvořák, Kráľ y Thomas (2010); Grohe, Kreutzer y Siebertz (2014).
16. Pikhurko, Spencer y Verbitsky (2006).
17. Pikhurko y Verbitsky (2011).
18. Verbitsky (2005).
19. Immerman y Lander (1990).
20. Ebbinghaus y Flum (1995). Parys (2014) escribe que este resultado de indecidibilidad es bien conocido y lo atribuye a Trahtenbrot (1950) sobre la indecidibilidad de la satisfacibilidad de primer orden para clases más generales de estructuras finitas.
21. Lavrov (1963).
22. Grohe (2017), págs.
23. Grohe (2017), págs.
24. Cai, Fürer y Immerman (1992).
25. Hella, Kolaitis y Luosto (1996).
26. Laubner (2010).
27. Estas definiciones se pueden encontrar, por ejemplo, en Courcelle & Engelfriet (2012), p. 69, bajo la notación ligeramente diferente MS ₁ y MS _2. Otros autores utilizaron las notaciones MSO ₁ y MSO ₂ , y Courcelle también las utilizó más tarde; véase, por ejemplo, Courcelle (2018).
28. Fagin, Stockmeyer y Vardi (1995).
29. Courcelle y Engelfriet (2012); Libkin (2004), Corolario 7.24, págs. 126-127.
30. Courcelle (1996).
31. Courcelle y Engelfriet (2012).
32. Elberfeld, Jakoby y Tantau (2010).
33. Grohe (2001); Kawarabayashi y Reed (2007).
34. Courcelle y Oum (2007).
35. Versión en inglés.

Referencias

• Bruggink, HJ Sander; König, Barbara (2018), "Lenguajes reconocibles de flechas y cospans", Estructuras matemáticas en informática , 28 (8): 1290–1332, doi :10.1017/S096012951800018X, MR  3849613, S2CID  52275704
• Cai, Jin-Yi; Fürer, Martin; Immerman, Neil (1992), "Un límite inferior óptimo para el número de variables para la identificación de gráficos", Combinatorica , 12 (4): 389–410, doi :10.1007/BF01305232, MR  1194730
• Chen, Jianer; Huang, Xiuzhen; Kanj, Iyad A.; Xia, Ge (2006), "Límites inferiores computacionales fuertes a través de la complejidad parametrizada", Journal of Computer and System Sciences , 72 (8): 1346–1367, doi : 10.1016/j.jcss.2006.04.007
• Courcelle, Bruno (1996), "Sobre la expresión de propiedades de grafos en algunos fragmentos de lógica monádica de segundo orden" (PDF) , en Immerman, Neil ; Kolaitis, Phokion G. (eds.), Proc. Descr. Complex. Finite Models , DIMACS, vol. 31, Amer. Math. Soc., págs. 33–62, CiteSeerX  10.1.1.55.5184 , MR  1451381
• Courcelle, Bruno ; Engelfriet, Joost (2012), Estructura de grafos y lógica monádica de segundo orden: un enfoque teórico del lenguaje , Enciclopedia de matemáticas y sus aplicaciones, vol. 138, Cambridge University Press , ISBN 9781139644006, Zbl1257.68006 ​
• Courcelle, Bruno (2018), "Autómatas voladores para comprobar las propiedades de los gráficos MSO ₂ ", Discrete Applied Mathematics , 245 : 236–252, arXiv : 1511.08605 , doi : 10.1016/j.dam.2016.10.018, MR  3804787
• Courcelle, Bruno ; Oum, Sang-il (2007), "Vertex-menors, lógica monádica de segundo orden y una conjetura de Seese" (PDF) , Journal of Combinatorial Theory , Serie B, 97 (1): 91–126, doi : 10.1016/j.jctb.2006.04.003 , MR  2278126
• Downey, RG ; Fellows, MR (1995), "Tratabilidad y completitud de parámetros fijos. II. Sobre completitud para W[1]", Theoretical Computer Science , 141 (1–2): 109–131, doi : 10.1016/0304-3975(94)00097-3
• Dvořák, Zdeněk ; Kráľ, Daniel ; Thomas, Robin (2010), "Decidir propiedades de primer orden para grafos dispersos", Proc. 51.° Simposio anual IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 133–142, CiteSeerX  10.1.1.170.9781 , doi :10.1109/FOCS.2010.20, ISBN 978-0-7695-4244-7, MR  3024787, S2CID  15264036
• Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995), Teoría de modelos finitos , Springer Monographs in Mathematics (2.ª ed.), Springer, pág. 129, doi :10.1007/3-540-28788-4
• Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (octubre de 2010), "Versiones en espacio logarítmico de los teoremas de Bodlaender y Courcelle" (PDF) , Proc. 51.° Simposio anual IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 143-152, doi :10.1109/FOCS.2010.21, S2CID  1820251
• Fagin, Ronald (1976), "Probabilidades en modelos finitos", Journal of Symbolic Logic , 41 (1): 50–58, doi :10.1017/s0022481200051756, JSTOR  2272945, MR  0476480, S2CID  2563318
• Fagin, Ronald ; Stockmeyer, Larry J. ; Vardi, Moshe Y. (1995), "Sobre NP monádico vs. co-NP monádico", Información y Computación , 120 (1): 78–92, doi : 10.1006/inco.1995.1100 , MR  1340807
• Glebskiĭ, Ju. V.; Kogan, DI; Liogon'kiĭ, MI; Talanov, VA (1969), "Volumen y fracción de satisfacibilidad de fórmulas del cálculo de predicados inferiores", Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika (2): 17–27, MR  0300882
• Goldberg, Leslie Ann (1993), "Algoritmos de retardo polinomial en el espacio polinomial para el listado de familias de grafos", Actas del vigésimo quinto simposio anual de la ACM sobre teoría de la computación (STOC '93) , Nueva York, NY, EE. UU.: ACM, págs. 218-225, doi : 10.1145/167088.167160, ISBN 0-89791-591-7, S2CID6305108 ​
• Grandjean, Étienne (1983), "Complejidad de la teoría de primer orden de casi todas las estructuras finitas", Información y Control , 57 (2–3): 180–204, doi : 10.1016/S0019-9958(83)80043-6 , MR  0742707
• Grohe, Martin (2001), "Cálculo de números cruzados en tiempo cuadrático", Actas del Trigésimo Tercer Simposio Anual de la ACM sobre Teoría de la Computación (STOC '01) , págs. 231–236, arXiv : cs/0009010 , doi :10.1145/380752.380805, S2CID  724544
• Grohe, Martin (2017), Complejidad descriptiva, canonización y teoría de la estructura de grafos definibles , Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, Sr.  3729479
• Grohe, Martin ; Kreutzer, Stephan; Siebertz, Sebastian (2014), "Decidir propiedades de primer orden de grafos densos en ninguna parte", Actas del 46.º Simposio anual de la ACM sobre teoría de la computación (STOC '14) , Nueva York: ACM, págs. 89–98, arXiv : 1311.3899 , doi :10.1145/2591796.2591851, ISBN 978-1-4503-2710-7, Número de identificación del sujeto  13297133
• Hella, Lauri; Kolaitis, Phokion G.; Luosto, Kerkko (1996), "Equivalencia casi en todas partes de lógicas en la teoría de modelos finitos", The Bulletin of Symbolic Logic , 2 (4): 422–443, doi :10.2307/421173, JSTOR  421173, MR  1460316, S2CID  16411368
• Henson, C. Ward (1972), "Estructuras relacionales homogéneas contables y teorías categóricas", The Journal of Symbolic Logic , 37 : 494–500, doi :10.2307/2272734, JSTOR  2272734, MR  0321727, S2CID  40662635 ${\displaystyle \aleph _{0}}$
• Immerman, Neil ; Lander, Eric (1990), "Descripción de grafos: un enfoque de primer orden para la canonización de grafos", en Selman, Alan L. (ed.), Complexity Theory Retrospective: In honor of Juris Hartmanis on the occasion of his sixtieth birthday , Nueva York: Springer-Verlag, págs. 59–81, doi :10.1007/978-1-4612-4478-3_5, MR  1060782
• Lavrov, IA (1963), "La no separabilidad efectiva del conjunto de fórmulas idénticamente verdaderas y el conjunto de fórmulas finitamente refutables para ciertas teorías elementales", Algebra i Logika Sem. , 2 (1): 5–18, MR  0157904
• Kawarabayashi, Ken-ichi ; Reed, Bruce (2007), "Computing crossing number in linear time", Actas del Trigésimo Noveno Simposio Anual de la ACM sobre Teoría de la Computación (STOC '07) , págs. 382–390, doi :10.1145/1250790.1250848, S2CID  13000831
• Koncewicz, Leszek (1973), "Definibilidad de clases de grafos en el cálculo de predicados de primer orden con identidad", Academia Polaca de Ciencias , 32 : 159–190, doi :10.1007/BF02123839, JSTOR  20014678, MR  0351796, S2CID  189786935
• Laubner, Bastian (2010), "Captura de tiempo polinomial en gráficos de intervalos", 25.° Simposio anual IEEE sobre lógica en informática (LICS 2010) , Los Alamitos, California: IEEE Computer Society, págs. 199-208, arXiv : 0911.3799 , doi : 10.1109/LICS.2010.42, MR  2963094, S2CID  1450409
• Libkin, Leonid (2004), Elementos de la teoría de modelos finitos , Textos en informática teórica: una serie EATCS, Springer-Verlag, Berlín, doi : 10.1007/978-3-662-07003-1, ISBN 3-540-21202-7, MR  2102513, S2CID  30176939
• Lynch, James F. (1992), "Probabilidades de oraciones sobre gráficos aleatorios muy dispersos", Random Structures & Algorithms , 3 (1): 33–53, doi :10.1002/rsa.3240030105, MR  1139487
• Nešetřil, Jaroslav ; Ossona de Mendez, Patrice (2012), Sparsity: Graphs, Structures, and Algorithms , Algorithms and Combinatorics, vol. 28, Springer-Verlag, doi :10.1007/978-3-642-27875-4, ISBN 978-3-642-27874-7, Sr.  2920058
• Parys, Paweł (2014), "Lógica de primer orden en grafos CPDA", Ciencias de la computación: teoría y aplicaciones , Lecture Notes in Computer Science , vol. 8476, Nueva York: Springer-Verlag, págs. 300–313, doi :10.1007/978-3-319-06686-8_23, MR  3218557, S2CID  31640587
• Pikhurko, Oleg; Spencer, Joel ; Verbitsky, Oleg (2006), "Definiciones sucintas en la teoría de grafos de primer orden", Annals of Pure and Applied Logic , 139 (1–3): 74–109, arXiv : math/0401307 , doi :10.1016/j.apal.2005.04.003, MR  2206252, S2CID  3041191
• Pikhurko, Oleg; Verbitsky, Oleg (2011), "Complejidad lógica de grafos: un estudio", en Grohe, Martin ; Makowsky, Johann A. (eds.), Métodos teóricos de modelos en combinatoria finita (Sesión especial conjunta AMS-ASL, 5-8 de enero de 2009, Washington, DC) , Contemporary Mathematics, vol. 558, American Mathematical Society, págs. 129–180, arXiv : 1003.4865 , ISBN 978-0-8218-8322-8
• Seese, D. (1991), "La estructura de los modelos de teorías monádicas decidibles de grafos", Annals of Pure and Applied Logic , 53 (2): 169–195, doi : 10.1016/0168-0072(91)90054-P , MR  1114848
• Shelah, Saharon ; Spencer, Joel (1988), "Leyes cero-uno para gráficos aleatorios dispersos", Journal of the American Mathematical Society , 1 (1): 97–115, doi : 10.2307/1990968 , JSTOR  1990968, MR  0924703
• Spencer, Joel (1990), "Espectros infinitos en la teoría de grafos de primer orden", Combinatorica , 10 (1): 95–102, doi :10.1007/BF02122699, MR  1075070, S2CID  27770505
• Spencer, Joel (2001), La extraña lógica de los grafos aleatorios , Algorithms and Combinatorics, vol. 22, Springer-Verlag, Berlín, doi :10.1007/978-3-662-04538-1, ISBN 3-540-41654-4, Sr.  1847951
• Trahtenbrot, BA (1950), "La imposibilidad de un algoritmo para el problema de decisión para dominios finitos", Doklady Akademii Nauk SSSR , New Series, 70 : 569–572, MR  0033784
• Verbitsky, Oleg (2005), "La definibilidad de primer orden de gráficos con separadores a través del juego de Ehrenfeucht", Theoretical Computer Science , 343 (1–2): 158–176, arXiv : math/0401361 , doi :10.1016/j.tcs.2005.05.003, MR  2168849, S2CID  17886484
• Verbitsky, Oleg; Zhukovskii, Maksim (2019), "Límites estrictos en la complejidad descriptiva asintótica del isomorfismo de subgrafos", ACM Transactions on Computational Logic , 20 (2): A9:1–A9:18, arXiv : 1802.02143 , doi :10.1145/3303881, MR  3942556, S2CID  3603039
• Zeume, Thomas (2017), "La complejidad descriptiva dinámica de la k-clique" (PDF) , Información y Computación , 256 : 9–22, doi :10.1016/j.ic.2017.04.005, MR  3705411, S2CID  1412001