En los campos matemáticos de la teoría de grafos y la teoría de modelos finitos , la lógica de los grafos se ocupa de las especificaciones formales de las propiedades de los grafos utilizando fórmulas de lógica matemática . Hay varias variaciones en los tipos de operaciones lógicas que se pueden utilizar en estas fórmulas. La lógica de primer orden de los gráficos se refiere a fórmulas en las que las variables y los predicados se refieren a vértices y bordes individuales de un gráfico, mientras que la lógica de gráficos monádica de segundo orden permite la cuantificación sobre conjuntos de vértices o bordes. Lógicas basadas en el punto mínimo fijo Los operadores permiten predicados más generales sobre tuplas de vértices, pero estos predicados solo pueden construirse a través de operadores de punto fijo, restringiendo su poder a un nivel intermedio entre el primer orden y el segundo orden monádico.
Una sentencia puede ser verdadero para algunos gráficos y falso para otros; un gráficose dice que modela , escrito , Si es cierto de los vértices y la relación de adyacencia de . El problema algorítmico de la verificación de modelos se refiere a probar si un gráfico dado modela una oración determinada. El problema algorítmico de la satisfacibilidad se refiere a probar si existe un gráfico que modele una oración determinada. Aunque tanto la verificación del modelo como la capacidad de satisfacción son difíciles en general, varios metateoremas algorítmicos importantes muestran que las propiedades expresadas de esta manera pueden probarse de manera eficiente para clases importantes de gráficos.
Otros temas de investigación en la lógica de los gráficos incluyen investigaciones sobre la probabilidad de que un gráfico aleatorio tenga una propiedad especificada dentro de un tipo particular de lógica y métodos para la compresión de datos basados en la búsqueda de fórmulas lógicas modeladas por un gráfico único.
Primer orden
En la lógica de primer orden de los gráficos, una propiedad de gráfico se expresa como una fórmula lógica cuantificada cuyas variables representan los vértices del gráfico , con predicados para las pruebas de igualdad y adyacencia.
Ejemplos de
Por ejemplo, la condición de que un gráfico no tenga vértices aislados puede expresarse mediante la oración
donde el El símbolo indica la relación de adyacencia no dirigida entre dos vértices. Esta oración se puede interpretar en el sentido de que para cada vértice hay otro vértice que es adyacente a . [1]
El problema de isomorfismo de subgrafo para un subgrafo fijo H pregunta si H aparece como subgrafo de un grafo G mayor . Puede expresarse mediante una oración que establece la existencia de vértices (uno por cada vértice de H ) de manera que, para cada arista de H , el par de vértices correspondiente son adyacentes; ver foto. Como caso especial, el problema de la camarilla (para un tamaño de camarilla fijo) puede expresarse mediante una oración que establece la existencia de un número de vértices igual al tamaño de la camarilla, todos los cuales son adyacentes.
Axiomas
Para gráficos simples no dirigidos , la teoría de gráficos de primer orden incluye los axiomas
Otros tipos de gráficos, como los gráficos dirigidos , pueden involucrar diferentes axiomas, y las formulaciones lógicas de propiedades multigráficas requieren tener variables separadas para vértices y aristas.
Ley cero uno
Glebskiĭ y col. (1969) e, independientemente, Fagin (1976) demostraron una ley de cero a uno para la lógica de grafos de primer orden; La demostración de Fagin utilizó el teorema de la compacidad . De acuerdo con este resultado, cada oración de primer orden es casi siempre verdadera o casi siempre falsa para gráficos aleatorios en el modelo Erd –s-Rényi . Es decir, sea S una oración fija de primer orden y elija un gráfico aleatorio de n -vértices G n uniformemente al azar entre todos los gráficos de un conjunto de n vértices etiquetados. Entonces, en el límite cuando n tiende a infinito, la probabilidad de que los modelos G n S tiendan a cero oa uno:
Además, existe un gráfico infinito específico, el gráfico Rado R , de modo que las oraciones modeladas por el gráfico Rado son exactamente aquellas para las que la probabilidad de ser modeladas por un gráfico finito aleatorio tiende a uno:
Para gráficos aleatorios en los que cada borde se incluye independientemente de los demás con una probabilidad fija, el mismo resultado es verdadero, con las mismas oraciones que tienen probabilidades que tienden a cero o uno.
La complejidad computacional de determinar si una oración dada tiene una probabilidad que tiende a cero oa uno es alta: el problema es PSPACE-completo . [3] Si una propiedad de 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 n -vértices que modelan la propiedad, con un retardo polinomial (en función de n ) por gráfico. [2]
Se puede realizar un análisis similar para gráficos 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 de forma independiente con igual probabilidad para todas las aristas. Sin embargo, para estos gráficos 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 borde se aleja del umbral, la probabilidad de tener la propiedad dada tiende a cero o uno. Estos umbrales nunca pueden ser una potencia irracional de n , por lo que los gráficos aleatorios en los que la probabilidad de inclusión del borde es una potencia irracional obedecen a una ley de cero uno análoga a la de los gráficos uniformemente aleatorios. Una ley similar de cero-uno es válida para gráficos aleatorios muy dispersos que tienen una probabilidad de inclusión de aristas de n - c con c > 1 , siempre que c no sea una razón superparticular . [4] Si c es superparticular, la probabilidad de tener una propiedad dada puede tender a un límite que no sea cero o uno, pero este límite se puede calcular de manera eficiente. [5] Existen oraciones de primer orden que tienen infinitos umbrales. [6]
Complejidad parametrizada
Si una oración de primer orden incluye k variables distintas, entonces la propiedad que describe puede probarse en gráficas de n vértices examinando todas las k -tuplas de vértices; sin embargo, este algoritmo de búsqueda de fuerza bruta no es particularmente eficiente y toma tiempo O ( n k ) . El problema de comprobar si una gráfica modela una oración de primer orden incluye como casos especiales el problema de isomorfismo de subgrafo (en el que la oración describe las gráficas que contienen un subgrafo fijo) y el problema de camarilla (en el que la oración describe gráficas que contienen gráficos completos). subgrafos 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 que tenga un algoritmo manejable de parámetros fijos, uno cuyo tiempo de ejecución tome la forma O ( f ( k ) n c ) para una función f y constante c que sean independientes de k y n . [7] 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 tomarían necesariamente un tiempo proporcional a una potencia de n cuyo exponente es proporcional a k . [8]
En clases restringidas de gráficos, la verificación de modelos de oraciones de primer orden puede ser mucho más eficiente. En particular, cada propiedad gráfica expresable como una oración de primer orden se puede probar en tiempo lineal para las gráficas de expansión acotada . Estos son los gráficos en los que todos los menores superficiales son gráficos dispersos , con una relación de aristas a vértices delimitados por una función de la profundidad del menor. Incluso de manera más general, la verificación del modelo de primer orden se puede realizar en un tiempo casi lineal para gráficos de densidad nula, clases de gráficos para los cuales, en cada profundidad posible, hay al menos un menor superficial prohibido. Por el contrario, si la verificación del modelo es manejable con parámetros fijos para cualquier familia hereditaria de gráficos, esa familia no debe ser densa en ninguna parte. [9]
Compresión de datos e isomorfismo de gráficos
A primera frase orden S en la lógica de gráficos se dice para definir un gráfico G si G es el único gráfico que modelos S . Cada gráfico puede estar definido por al menos una oración; por ejemplo, se puede definir un gráfico G de n -vértices mediante una oración con n + 1 variables, una para cada vértice del gráfico, y una más para establecer la condición de que no haya vértices distintos de los n vértices del gráfico. Cláusulas adicionales de la frase se pueden utilizar para asegurar que no hay dos variables de vértice son iguales, que cada borde de G está presente, y no existe ningún borde entre un par de vértices no adyacentes de G . Sin embargo, para algunos gráficos existen fórmulas significativamente más cortas que definen el gráfico. [10]
Se pueden definir varios invariantes de gráfico diferentes a partir de las oraciones más simples (con diferentes medidas de simplicidad) que definen un gráfico dado. En particular, la profundidad lógica de un gráfico se define como el nivel mínimo de anidamiento de cuantificadores (el rango del cuantificador ) en una oración que define el gráfico. [11] La oración descrita anteriormente anida los cuantificadores para todas sus variables, por lo que tiene una profundidad lógica n + 1 . El ancho lógico de un gráfico es el número mínimo de variables en una oración que lo define. [11] En la oración descrita anteriormente, este número de variables es nuevamente n + 1 . Tanto la profundidad lógica como el ancho lógico se pueden limitar en términos del ancho del árbol del gráfico dado. [12] La longitud lógica, de manera análoga, se define como la longitud de la fórmula más corta que describe el gráfico. [11] La oración descrita anteriormente tiene una longitud proporcional al cuadrado del número de vértices, pero es posible definir cualquier gráfico mediante una fórmula con una longitud proporcional a su número de aristas.
Todos los árboles y la mayoría de los gráficos pueden describirse mediante oraciones de primer orden con solo dos variables, pero ampliadas contando predicados. Para gráficos que pueden describirse mediante oraciones en esta lógica con un número constante fijo de variables, es posible encontrar una canonización de gráfico 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. [13]
Satisfacción
Es indecidible si una oración dada de primer orden puede realizarse mediante un gráfico finito no dirigido. [14]
Existen oraciones de primer orden que se modelan mediante gráficos infinitos, pero no mediante ningún gráfico finito. Por ejemplo, la propiedad de tener exactamente un vértice de grado uno, con todos los demás vértices de grado exactamente dos, puede expresarse mediante una oración de primer orden. Está modelado por un rayo infinito , pero viola el lema del apretón de manos de Euler para gráficos finitos. Sin embargo, de la solución negativa del Entscheidungsproblem (por Alonzo Church y Alan Turing en la década de 1930) se sigue que la satisfacibilidad de oraciones de primer orden para gráficos que no están constreñidos a ser finitos sigue siendo indecidible. También es indecidible distinguir entre las oraciones de primer orden que son verdaderas para todas las gráficas y las que son verdaderas para gráficas finitas pero falsas para algunas gráficas infinitas. [15]
Punto fijo
Las lógicas de gráficos basadas en el punto mínimo fijo amplían la lógica de los gráficos de primer orden al permitir predicados definidos por operadores especiales de punto fijo, que definen un predicado como el punto fijo de una fórmula que relaciona los valores del predicado con otros valores del mismo predicado. Por ejemplo, si es un predicado que determina si dos vértices están conectados por una ruta en un gráfico dado, entonces 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 menos fijo significa que los pares de vértices para los quees verdadero son un subconjunto de los pares de vértices para los que cualquier otro punto fijo de la misma fórmula es verdadero. En la lógica de punto mínimo fijo, el lado derecho de la fórmula de definición debe usar el predicado solo de manera positiva (es decir, cada apariencia debe estar anidada dentro de un número par de negaciones) para que el punto menos fijo esté bien definido. En una variante equivalente, la lógica inflacionaria de punto fijo, la fórmula no necesita ser monótona, pero el punto fijo resultante se define como el que se obtiene aplicando repetidamente las implicaciones derivadas de la fórmula definitoria a partir del predicado todo falso. También son posibles otras variantes, que permiten implicaciones negativas o múltiples predicados definidos simultáneamente, pero no proporcionan un poder definitorio adicional. Un predicado, definido de una de estas formas, se puede aplicar a una tupla de vértices como parte de una fórmula lógica más grande. [dieciséis]
Lógicas de punto fijo, y extensiones de estas lógicas que también permiten contar con 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 problemas de decisión en teoría de grafos que puedan decidirse. 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 gráfico modela una fórmula en esta lógica puede siempre se decidirá en tiempo polinomial. No todas las propiedades del gráfico de tiempo polinomial se pueden modelar mediante una fórmula en una lógica que usa solo puntos fijos y conteo. [17] [18] Sin embargo, para algunas clases especiales de gráficos, las propiedades de tiempo polinomial son las mismas que las propiedades expresables en lógica de punto fijo con conteo. Estos incluyen gráficos aleatorios, [17] [19] gráficos de intervalo , [17] [20] y (a través de una expresión lógica del teorema de la estructura del gráfico ) todas las clases de gráficos caracterizados por menores prohibidos . [17]
Segundo orden
En la lógica monádica de segundo orden de los gráficos, las variables representan objetos de hasta cuatro tipos: vértices, aristas, conjuntos de vértices y conjuntos de aristas. Hay dos variaciones principales de la lógica de gráficos monádicos de segundo orden: MSO 1 en el que solo se permiten variables de vértice y conjunto de vértices, y MSO 2 en el que se permiten los cuatro tipos de variables. Los predicados de estas variables incluyen pruebas de igualdad, pruebas de pertenencia e incidencia de vértice-borde (si se permiten las variables de vértice y de borde) o adyacencia entre pares de vértices (si solo se permiten variables de vértice). Las variaciones adicionales en la definición permiten predicados adicionales, como predicados de conteo modular.
Ejemplos de
Como ejemplo, la conectividad de un grafo no dirigido se puede expresar en MSO 1 como la afirmación de que, para cada partición de los vértices en dos subconjuntos no vacíos, existe un borde de un subconjunto al otro. Una partición de los vértices puede describirse mediante el subconjunto S de vértices en un lado de la partición, y cada subconjunto debe describir una partición trivial (una en la que uno u otro lado está vacío) o estar cruzado por un borde. Es decir, un gráfico está conectado cuando modela la fórmula MSO 1
Sin embargo, la conectividad no se puede expresar en lógica gráfica de primer orden, ni tampoco en MSO 1 existencial (el fragmento de MSO 1 en el que todos los cuantificadores establecidos son existenciales y ocurren al comienzo de la oración) ni siquiera MSO 2 existencial . [21]
La hamiltonicidad se puede expresar en MSO 2 por la existencia de un conjunto de aristas que forman un gráfico regular 2 conectado en todos los vértices, con conectividad expresada como se indica arriba y regularidad 2 expresada como la incidencia de dos pero no tres aristas distintas en cada uno. vértice. Sin embargo, la hamiltonicidad no se puede expresar en MSO 1 , porque MSO 1 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 desbalanceados (que no lo son). [22]
Aunque no forma parte de la definición de MSO 2 , las orientaciones de gráficos no dirigidos se pueden representar mediante una técnica que involucra árboles Trémaux . Esto permite que se expresen también otras propiedades gráficas que involucran orientaciones. [23]
Teorema de Courcelle
De acuerdo con el teorema de Courcelle , cada propiedad fija de MSO 2 puede probarse en tiempo lineal en gráficos de ancho de árbol acotado , y cada propiedad fija de MSO 1 puede probarse en tiempo lineal en gráficos de ancho de camarilla acotado . [24] La versión de este resultado para gráficos de ancho de árbol acotado también se puede implementar en espacio logarítmico . [25] Las aplicaciones de este resultado incluyen un algoritmo manejable de parámetros fijos para calcular el número de cruce de un gráfico. [26]
Teorema de Seese
El problema de satisfacibilidad para una fórmula de lógica monádica de segundo orden es el problema de determinar si existe al menos un gráfico (posiblemente dentro de una familia restringida de gráficos) para el que la fórmula es verdadera. Para familias de grafos arbitrarios y fórmulas arbitrarias, este problema es indecidible . Sin embargo, la satisfacibilidad de las fórmulas de MSO 2 es decidible para los gráficos de ancho de árbol acotado, y la satisfacibilidad de las fórmulas de MSO 1 es decidible para gráficos de ancho de camarilla acotado. La demostración 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 gráfico que pueda aceptar.
Como recíproco parcial, Seese (1991) demostró que, siempre que una familia de gráficos tiene un problema de satisfacibilidad de MSO 2 decidible , la familia debe tener un ancho de árbol acotado. La demostración se basa en un teorema de Robertson y Seymour de que las familias de gráficos con un ancho de árbol ilimitado tienen menores de cuadrícula arbitrariamente grandes . Seese también conjeturaba que cada familia de gráficos con un problema de satisfacibilidad de MSO 1 decidible debe tener un ancho de camarilla acotado; esto no ha sido probado, pero un debilitamiento de la conjetura que extiende MSO 1 con predicados de conteo modular es cierto. [27]
Notas
- ^ Spencer (2001) , Sección 1.2, "¿Qué es una teoría de primer orden?", Págs. 15-17 .
- ↑ a b Goldberg (1993) .
- ^ Grandjean (1983) .
- ^ Shelah y Spencer (1988) ; Spencer (2001) .
- ^ Lynch (1992) .
- ^ Spencer (1990) .
- ^ Downey y becarios (1995) .
- ^ Chen y col. (2006) .
- ^ Nešetřil y Ossona de Mendez (2012) , 18.3 El problema del isomorfismo del subgrafo y consultas booleanas, págs. 400–401; Dvořák, Kráľ y Thomas (2010) ; Grohe, Kreutzer y Siebertz (2014) .
- ^ Pikhurko, Spencer y Verbitsky (2006) .
- ↑ a b c Pikhurko y Verbitsky (2011) .
- ^ Verbitsky (2005) .
- ^ Immerman y Lander (1990) .
- ↑ 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.
- ^ Lavrov (1963) .
- ^ Grohe (2017) , págs. 23-27.
- ↑ a b c d Grohe (2017) , págs. 50–51.
- ^ Cai, Fürer e Immerman (1992) .
- ^ Hella, Kolaitis y Luosto (1996) .
- ^ Laubner (2010) .
- ^ Fagin, Stockmeyer y Vardi (1995) .
- ^ Courcelle y Engelfriet (2012) ; Libkin (2004) , Corolario 7.24, págs. 126-127 .
- ^ Courcelle (1996) .
- ^ Courcelle y Engelfriet (2012) .
- ^ Elberfeld, Jakoby y Tantau (2010) .
- ^ Grohe (2001) ; Kawarabayashi y Reed (2007) .
- ^ Courcelle y Oum (2007) .
Referencias
- Cai, Jin-Yi; Fürer, Martin; Immerman, Neil (1992), "Un límite inferior óptimo en el número de variables para la identificación del gráfico", 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 gráficas en algunos fragmentos de lógica monádica de segundo orden" (PDF) , en Immerman, Neil ; Kolaitis, Phokion G. (eds.), Proc. Descr. Complejo. Modelos finitos , DIMACS, 31 , Amer. Matemáticas. Soc., Págs. 33-62, MR 1451381.
- Courcelle, Bruno ; Engelfriet, Joost (2012), Estructura gráfica y lógica monádica de segundo orden: un enfoque teórico del lenguaje , Enciclopedia de las matemáticas y sus aplicaciones, 138 , Cambridge University Press , ISBN 9781139644006, Zbl 1257.68006.
- Courcelle, Bruno ; Oum, Sang-il (2007), "Vértices menores, 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]", Informática teórica , 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 gráficos dispersos", Proc. 51º Simposio anual del IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 133-142, MR 3024787.
- Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (octubre de 2010), "Versiones de espacio de registro de los teoremas de Bodlaender y Courcelle" (PDF) , Proc. 51 ° Simposio anual del IEEE sobre fundamentos de la informática (FOCS 2010) , págs. 143-152, doi : 10.1109 / FOCS.2010.21.
- Fagin, Ronald (1976), "Probabilidades en modelos finitos" (PDF) , Journal of Symbolic Logic , 41 (1): 50–58, doi : 10.1017 / s0022481200051756 , MR 0476480.
- Fagin, Ronald ; Stockmeyer, Larry J .; Vardi, Moshe Y. (1995), "On monadic NP vs monadic co-NP", Information and Computation , 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 predicado inferior", Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika (2): 17-27, MR 0300882.
- Goldberg, Leslie Ann (1993), "Algoritmos de retardo polinomial del espacio polinómico para enumerar familias de gráficos", Actas del vigésimo quinto Simposio Anual de 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.
- 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), "Computación de números cruzados en tiempo cuadrático", Actas del trigésimo tercer Simposio Anual de ACM sobre Teoría de la Computación (STOC '01) , págs. 231-236, arXiv : cs / 0009010 , doi : 10.1145 /380752.380805.
- Grohe, Martin (2017), Complejidad descriptiva, canonización y teoría de la estructura gráfica definible , Lecture Notes in Logic, 47 , Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479.
- Grohe, Martin ; Kreutzer, Stephan; Siebertz, Sebastian (2014), "Decidir las propiedades de primer orden de los gráficos densos en ninguna parte", Actas del 46º Simposio Anual de 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.
- Hella, Lauri; Kolaitis, Phokion G .; Luosto, Kerkko (1996), "Casi en todas partes equivalencia de lógicas en la teoría de modelos finitos", The Bulletin of Symbolic Logic , 2 (4): 422–443, doi : 10.2307 / 421173 , MR 1460316.
- Immerman, Neil ; Lander, Eric (1990), "Describing graphs: a first-order approach to graph canonization", en Selman, Alan L. (ed.), Complexity Theory Retrospective: In honor of Juris Hartmanis con motivo de su sexagésimo cumpleaños , New 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), "Computación del número de cruce en tiempo lineal", Actas del trigésimo noveno Simposio Anual de ACM sobre Teoría de la Computación (STOC '07) , págs. 382–390, doi : 10.1145 / 1250790.1250848.
- Laubner, Bastian (2010), "Capturing polynomial time on interval graphs", 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010) , Los Alamitos, California: IEEE Computer Society, págs. 199-208, arXiv : 0911.3799 , doi : 10.1109 / LICS.2010.42 , MR 2963094.
- 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.
- Lynch, James F. (1992), "Probabilidades de oraciones sobre gráficos aleatorios muy dispersos", Estructuras y algoritmos aleatorios , 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, 28 , Springer-Verlag, doi : 10.1007 / 978-3-642-27875-4 , hdl : 10338.dmlcz / 143192 , ISBN 978-3-642-27874-7, MR 2920058.
- Parys, Paweł (2014), "Lógica de primer orden en gráficos CPDA", Ciencias de la computación: teoría y aplicaciones , Lecture Notes in Computer Science , 8476 , Nueva York: Springer-Verlag, págs. 300–313, doi : 10.1007 / 978 -3-319-06686-8_23 , MR 3218557.
- Pikhurko, Oleg; Spencer, Joel ; Verbitsky, Oleg (2006), "Definiciones sucintas en la teoría de gráficos 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 , Sr. 2206252.
- Pikhurko, Oleg; Verbitsky, Oleg (2011), "Complejidad lógica de los gráficos: una encuesta", en Grohe, Martin ; Makowsky, Johann A. (eds.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, 5-8 de enero de 2009, Washington, DC) , Contemporary Mathematics, 558 , American Mathematical Society, págs. 129–180.
- Seese, D. (1991), "La estructura de los modelos de teorías monádicas decidibles de gráficos", Annals of Pure and Applied Logic , 53 (2): 169-195, doi : 10.1016 / 0168-0072 (91) 90054- P , MR 1114848.
- Sela, 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 , MR 0924703.
- Spencer, Joel (1990), "Espectros infinitos en la teoría de gráficos de primer orden", Combinatorica , 10 (1): 95–102, doi : 10.1007 / BF02122699 , MR 1075070.
- Spencer, Joel (2001), La extraña lógica de gráficos aleatorios , algoritmos y combinatorios, 22 , Springer-Verlag, Berlín, doi : 10.1007 / 978-3-662-04538-1 , ISBN 3-540-41654-4, Señor 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 mediante el juego Ehrenfeucht", Ciencias de la computación teóricas , 343 (1–2): 158–176, doi : 10.1016 / j.tcs.2005.05.003 , MR 2168849.