Logique des graphes

Dans les domaines mathématiques de la théorie des graphes et de la théorie des modèles finis, la logique des graphes traite de la spécification formelle de propriétés de graphe en utilisant des propositions de la logique mathématique. Il existe plusieurs variantes suivant les types d'opérations logiques qui peuvent être utilisées dans ces propositions. La logique du premier ordre des graphes concerne les propositions dans lesquelles les variables et les prédicats concernent les sommets et les arêtes individuels d'un graphe, tandis que la logique monadique de graphe du second ordre permet une quantification sur des ensembles de sommets ou d'arêtes. Les logiques basées sur les plus petits opérateurs de point fixe permettent des prédicats plus généraux sur des tuples de sommets, mais ces prédicats ne peuvent être construits qu'en utilisant des opérateurs de point fixe, ce qui limite leur puissance.

Une proposition $S$ peut être vraie pour certains graphes et fausse pour d'autres; un graphe $G$ est un modèle de $S$, écrire $G\models S$, si $S$ est vraie sur les sommets et la relation d'adjacence de $G$. Le problème algorithmique de vérification du modèle (model checking) est relatif au fait de savoir si un graphe est un modèle d'une proposition donnée. Le problème algorithmique de satisfiabilité se demande s'il existe un graphe modélisant une proposition donnée. Bien que la vérification de modèle et la satisfiabilité soient difficiles en général, plusieurs méta-théorèmes algorithmiques majeurs montrent que les propriétés exprimées de cette manière peuvent être testées efficacement pour d'importantes classes de graphes.

D'autres sujets de recherche en logique des graphes incluent des études sur la probabilité qu'un graphe aléatoire modélise une proposition spécifiée pour un type particulier de logique, ainsi que des méthodes de compression des données s'intéressant à la recherche de propositions logiques modélisées par un graphe unique.

Logique du premier ordre

Le graphique illustré ici apparaît comme le sous-graphe d'un graphe non orienté $G$ si et seulement si $G$ modélise la proposition $\exists x_{1},x_{2},x_{3},x_{4}.$ $x_{1}\sim x_{2}$ $\land$ $x_{2}\sim x_{3}$ $\land$ $x_{3}\sim x_{1}$ $\land$ $x_{3}\sim x_{4}$ $\land$ $x_{1}\neq x_{4}$ $\land$ $x_{2}\neq x_{4}$.

Dans le logique du premier ordre sur les graphes, une propriété de graphe est exprimée sous la forme d'une phrase logique quantifiée dont les variables représentent les sommets du graphe, et reposant sur les prédicats d'égalité et d'adjacence.

Exemples

Par exemple, la condition qu'un graphe n'ait pas de sommets isolés peut être exprimée par la proposition :$$\forall u\exists v(u\sim v)$$où le $\sim$ symbole indique la relation d'adjacence non dirigée entre deux sommets. Cette proposition peut être interprétée comme signifiant que pour chaque sommet $u$ il existe un autre sommet $v$ qui lui est adjacent.

Le problème d'isomorphisme de sous-graphe pour un sous-graphe fixe $H$ cherche à déterminer si $H$ apparaît comme un sous-graphe dans un graphe $G$. Il peut être exprimé par une proposition qui énonce l'existence de sommets (un pour chaque sommet de $H$) tels que, pour chaque arête de $H$, la paire de variables correspondante représente des sommets adjacents et tels que, pour chaque paire restante de sommets de $H$, la paire de variables correspondante représente des sommets distincts ; voir l'illustration. Le problème de clique (pour une taille de clique fixe) en est un cas particulier, il peut être exprimé par une proposition indiquant l'existence d'un nombre de sommets égal à la taille de la clique qui soient tous adjacents entre eux.

Axiomes

Pour les graphes non orientés simples, la théorie du premier ordre des graphes inclut les axiomes

$\forall u{\bigl (}\lnot (u\sim u){\bigr )}$ (le graphe ne contient aucune boucle), et

$\forall u\forall v(u\sim v)\Rightarrow (v\sim u){\bigr )}$ (le graphe n'est pas orienté).

D'autres types de graphes, tels que les graphes orientés, peuvent impliquer des axiomes différents, et la formulation logique de propriété sur les multigraphes nécessitent un traitement spécial, comme avoir plusieurs relations de bord ou des variables séparées pour les sommets et les arêtes.

Loi zéro-un

Le Graphe de Rado, un graphe infini qui modélise exactement les propositions de la logique du premier ordre qui sont presque toujours vraies sur les graphes finis !

Glebskiĭ et al. (1969) et de manière indépentante, Fagin (1976) ont prouvés une loi zéro-un pour la logique du premier ordre sur les graphes ; la preuve de Fagin reposant sur le théorème de compacité. Ce résultat implique que toute proposition du premier ordre est ou bien presque toujours vraie, ou bien presque toujours fausse sur les graphes d'Erdös-Rényi. Ainsi, soit $S$ une proposition et $G_{n}$ un graphe pris aléatoirement parmi tous les graphes à $n$ sommets. Quand $n$ tend vers l'infini, la probabilité que $G_{n}$ soit un modèle de $S$ tend ou bien vers zéro ou bien vers un .$$\lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.$$De plus, il existe un graphe infini spécifique, le graphe de Rado $R$, tel que les propositions modélisées par le graphe de Rado sont exactement celles pour lesquelles la probabilité d'être modélisée par un graphe fini aléatoire tend vers un : $$R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]=1.$$Le même résultat reste vraie pour les graphes aléatoires binomiaux pour lesquels chaque arête est incluse indépendamment des autres avec une probabilité fixe. Et ceux sont les mêmes propositions qui tendent vers un (et donc vers zéro).

Déterminer si une proposition donnée a une probabilité tendant vers zéro ou vers un est un problème PSPACE-complet. Mais si une propriété de graphe du premier ordre a une probabilité tendant vers un pour les graphes aléatoires, alors il est possible de lister tous les graphes à $n$-sommets qui modélisent cette propriété, avec un retard polynomial (en fonction de $n$) par graphe.

Une analyse similaire peut être effectuée pour des graphes aléatoires non uniformes, où la probabilité d'inclure une arête est une fonction du nombre de sommets, et où la décision d'inclure ou d'exclure une arête est prise indépendamment avec une probabilité égale pour toutes les arêtes. Cependant, pour ces graphes, la situation est plus compliquée. Dans ce cas, une propriété du premier ordre peut avoir un ou plusieurs seuils, de sorte que lorsque la probabilité d'inclusion de chaque arête est bornée par ce seuil alors la probabilité d'avoir la propriété donnée tend vers zéro ou un. Ces seuils ne peuvent jamais être une puissance irrationnelle de $n$, donc les graphes aléatoires où la probabilité d'inclusion d'arête est une puissance irrationnelle obéissent à une loi zéro-un analogue à celle des graphes uniformément aléatoires. Une loi similaire zéro-un est valable pour les graphes aléatoires très clairsemés qui ont une probabilité d'inclusion d'arête de $n^{-c}$ avec $c>1$, tant que $c$ n'est pas un rapport superparticulaire. Si $c$ est superparticulaire, la probabilité d'avoir une propriété donnée peut tendre vers une limite qui n'est ni zéro ni un, mais cette limite peut être calculée efficacement. Il existe des propositions du premier ordre qui ont une infinité de seuils.

Complexité paramétrée

Si une proposition du premier ordre comprend $k$ variables distinctes, alors la propriété qu'elle décrit peut être testée dans des graphes de $n$ sommets en examinant tous les $k$-tuples de sommets ; cependant, cette recherche par force brute ne donne pas un algorithme particulièrement efficace, puisqu'il est de complexité $O(n^{k})$. Le problème de vérifier si un graphe modélise une proposition donnée du premier ordre inclut comme cas particuliers le problème d'isomorphisme de sous-graphe (dans lequel la phrase décrit les graphiques qui contiennent un sous-graphique fixe) et le problème de clique (dans lequel la phrase décrit des graphiques qui contiennent des sous-graphiques complets d'une taille fixe). Le problème de clique est reconnu difficile pour L(1), le premier niveau d'une hiérarchie de problèmes difficiles du point de vue de la complexité paramétrée. Par conséquent, il est peu probable qu'il existe un algorithme à paramètres fixes, dont le temps d'exécution prenne la forme $O(f(k)n^{c})$ pour une fonction $f$ et une constante $c$ qui soient indépendants de $k$ et $n$. Plus fortement, si l'hypothèse du temps exponentiel est vraie, alors la recherche de clique et donc la vérification d'un modèle du premier ordre prendraient nécessairement un temps proportionnel à une puissance de $n$ dont l'exposant est proportionnel à $k$.

Sur certaines classes restreintes de graphes, la vérification des propositions du premier ordre peut être beaucoup plus efficace. En particulier, chaque propriété de graphe exprimable sous la forme d'une proposition du premier ordre peut être testée en temps linéaire pour les graphes d'expansion limitée. C'est-à-dire les graphes pour lesquels tous les mineurs superficiels sont des graphes clairsemés, avec un rapport des arêtes aux sommets bornés par une fonction de la profondeur du mineur. Plus généralement encore, la vérification d'un modèle du premier ordre peut être effectuée en temps quasi linéaire pour des graphes denses nulle part, des classes de graphes pour lesquelles, à chaque profondeur possible, il existe au moins un mineur peu profond interdit. Inversement, s'il existe un algorithme permettant la vérification de toute proposition du premier ordre en temps polynomial pour une famille de graphe donnée, alors cette famille doit être nulle part dense.

Compression de données et isomorphisme de graphe

On dit qu'une proposition du premier ordre de la logique des graphes $S$, définit un graphe $G$ si $G$ est le seul graphe qui modélise $S$. Pour tout graphe il existe au moins une proposition le définissant ; par exemple, on peut définir n'importe quel $n$- graphe de sommet $G$ par une phrase avec $n+1$ variables, une pour chaque sommet du graphe, et une de plus pour indiquer la condition qu'il n'y a pas de sommet autre que les $n$ sommets de ce graphe. Des clauses supplémentaires sont ensuite ajoutées afin de s'assurer qu'il n'y a pas deux variables représentant le même sommet, que chaque arête de $G$ est présent, et qu'aucune arête n'existe qui ne soit pas dans $G$. Cependant, pour certains graphes, il existe des définitions reposant sur des propositions nettement plus courtes que cette version naïve.

Plusieurs invariants de graphe différent peuvent être définis à partir des propositions les plus simples (pour différentes notions de simplicité) qui définissent un graphe donné. En particulier le profondeur logique d'un graphe est défini comme étant le niveau minimum d'imbrication des quantificateurs (le rang du quantificateur) d'une proposition permettant de modéliser le graphe. La proposition naïve décrite décrite ci-dessus imbrique les quantificateurs de toutes ses variables, elle a donc une profondeur logique de $n+1$. Le largeur logique d'un graphe est définie comme le nombre minimum de variables dans une proposition qui le définit. Dans la proposition naïve décrite ci-dessus, ce nombre de variables est à nouveau de $n+1$. La profondeur logique et la largeur logique peuvent être bornées par une fonction de la largeur arborescente du graphe. De la même manière, la longueur logique est définie comme la longueur de la plus courte proposition modélisant le graphe. La proposition décrite ci-dessus a une longueur proportionnelle à $n^{2}$, mais il est toujours possible de définir un graphe par une proposition de longueur proportionnelle à son nombre d'arêtes.

Tous les arbres, et la plupart des graphes, peuvent être décrits par des propositions du premier ordre incluant seulement deux variables, mais étendues en comptant les prédicats. Pour les graphes qui peuvent être décrits par des propositions avec un nombre constant fixe de variables, il est possible de trouver une écriture canonique du graphe en temps polynomial (avec un exposant égal au nombre de variables). En comparant les canonisations, il est possible de résoudre le problème d'isomorphisme de graphe pour ces graphes en temps polynomial.

Satisfaisabilité

Déterminer s'il existe un graphe fini non orienté modélisant une proposition donnée est un problème indécidable. Cela signifie qu'il n'existe pas d'algorithme générique permettant de répondre correctement à cette question pour toutes les propositions.

Certaines proposition du premier ordre ne sont modélisées par aucun graphe fini mais peuvent l'être par des graphes infinis. Par exemple, la propriété d'avoir exactement un sommet de degré un, avec tous les autres sommets ayant exactement un degré 2, peut être exprimé par une proposition du premier ordre. Cette propriété viole le lemme des poignées de main d'Euler pour les graphes finis mais peut être représenté par un bout infini. Cependant, il résulte de la solution négative au Problème d'Entscheidungsproblem (par Alonzo Church et Alain Turing dans les années 1930), que la satisfaisabilité des propositions de la logique du premier ordre reste indécidable pour les graphes qui ne sont pas contraints à être finis. Il est également indécidable de faire la distinction entre les propositions du premier ordre qui sont vraies pour tous les graphes et celles qui sont vraies pour les graphes finis mais fausses pour certains graphes infinis.

Point fixe

Un sommet $x$ est dit faible (surligné en rouge) si, à au plus une exception près $y$, chacun de ses voisins $z$ est faible : selon la formule de point fixe $W(x)\leftarrow \exists y\forall z{\bigl (}x\sim z\Rightarrow (y=z\vee W(z)){\bigr )}$. Les sommets restants (en bleu) forment le 2-cœur du graphe.

Les logiques de graphe basées sur les plus petits points-fixes étendent la logique du premier ordre en autorisant les prédicats (propriétés des sommets ou des tuples de sommets) définis par des opérateurs de point-fixe spéciaux. Ce type de définition commence par une implication, une formule indiquant que lorsque certaines valeurs du prédicat sont vraies, d'autres le sont également. Un « point fixe » désigne alors prédicat pour lequel cette implication est valide. Il peut y avoir de nombreux points fixes, y compris le prédicat toujours vrai ; un « plus petit point fixe » est un point fixe qui a le moins de valeurs vraies possible. Plus précisément, ses valeurs vraies doivent l'être aussi pour tous les autres points fixes.

Par exemple, définissons la connexité : $C(u,v)$ comme vraie lorsque les deux sommets $u$ et $v$ sont connectés par un chemin dans un graphe donné, et faux sinon. Alors chaque sommet est connecté à lui-même, et quand $u$ est connecté à un voisin de $v$, il est également relié (par une étape de plus) à $v$. On peut exprimer ce raisonnement en termes logiques : $C$ est le plus petit point fixe de la formule$$C(u,v)\leftarrow {\Bigl (}(u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.$$Ici, être un point fixe signifie que la vérité du côté droit de la formule implique la vérité du côté gauche, comme le suggère la flèche d'implication inversée. Dans ce cas, être le plus petit point fixe, implique qu'aucun sommet ne sera défini comme connecté à moins que leur connexité ne provienne d'une utilisation répétée de cette implication.

Plusieurs variantes des logiques de point fixe ont été étudiées. Dans la logique du plus petit point fixe, le côté droit de l'opérateur $\leftarrow$ dans la formule de définition doit utiliser le prédicat uniquement de manière positive (c'est-à-dire que chaque occurrence doit être imbriquée dans un nombre pair de négations) afin de bien définir le plus petit point-fixe. La logique du point fixe inflationniste est une autre variante (dont la puissance logique est équivalente), pour cette dernière, la formule n'a pas besoin d'être monotone mais le point fixe résultant est défini comme celui obtenu en appliquant de manière répétée des implications dérivées de la formule de définition à partir du prédicat dont toutes les valeurs sont fausses. D'autres variantes, permettant des implications négatives ou plusieurs prédicats définis simultanément, sont également possibles, mais ne fournissent aucun pouvoir de définition supplémentaire. Un prédicat, défini de l'une de ces manières, peut ensuite être appliqué à un tuple de sommets dans le cadre d'une proposition logique plus large.

Les logiques de points fixes, et les extensions de ces logiques qui autorisent également à compter des variables entières dont les valeurs vont de 0 au nombre de sommets, ont été utilisées en complexité descriptive, dans une tentative de fournir une description logique des problèmes de décision en théorie des graphes qui peuvent être décidés en temps polynomial. Le point fixe d'une formule logique peut toujours être construit en temps polynomial. On utilise pour cela un algorithme qui ajoute à plusieurs reprises des tuples à l'ensemble des valeurs pour lesquelles le prédicat est vrai jusqu'à atteindre un point fixe. Ainsi décider si un graphe modélise une proposition dans cette logique peut toujours être décidé en temps polynomial. Il n'est toutefois pas possible de formulé une proposition de cette logique (point fixe et comptage) pour toutes les propriétés de graphe vérifiables en temps polynomial. Cependant, pour certaines classes spéciales de graphes, les propriétés vérifiable en temps polynomial sont les mêmes que les propriétés exprimables en logique de point fixe avec comptage. Ceux-ci incluent les graphes aléatoires, les graphes d'intervalles et (par une expression logique de la théorème de structure des graphes) chaque classe de graphes caractérisée par des mineurs interdits.

Deuxième ordre

Dans le logique monadique du second ordre sur les graphes, les variables représentent des objets de quatre types différents : sommets, arêtes, ensembles de sommets et ensembles d'arêtes. Il existe deux variantes principales de la logique des graphes monadiques du second ordre : MSO₁ dans lequel seules les variables d'ensemble de sommets et de sommets sont autorisées, et MSO₂ dans lequel les quatre types de variables sont autorisés. Les prédicats sur ces variables incluent les tests d'égalité, les tests d'appartenance et soit l'incidence sommet-arête (si les variables sommet et arête sont autorisées), soit la contiguïté entre des paires de sommets (si seules les variables sommet sont autorisées). Des variations supplémentaires dans la définition autorisent des prédicats supplémentaires tels que des prédicats de comptage modulaires.

Exemples

À titre d'exemple, le connexité d'un graphe non orienté peut être exprimé en MSO₁ comme la proposition : pour chaque partition des sommets en deux sous-ensembles non vides, il existe une arête d'un sous-ensemble à l'autre. Une partition des sommets peut être décrite par le sous-ensemble $S$ de sommets d'un côté de la partition, et chacun de ces sous-ensembles doit soit décrire une partition triviale (une partition dans laquelle l'un ou l'autre côté est vide), soit être traversé par une arête. C'est-à-dire qu'un graphique est connecté lorsqu'il modélise la proposition MSO₁ :$$\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 )}.$$Cependant, la connexité ne peut pas être exprimée dans une logique de graphe du premier ordre, ni dans une version existentielle de MSO₁ (le fragment de MSO₁ dans lequel tous les quantificateurs d'ensemble sont existentiels et apparaissent au début de la phrase) ni même dans une version existentielle de MSO₂.

L'existence d'une chaîne Hamiltonienne peut être exprimé dans MSO₂ par l'existence d'un ensemble d'arêtes qui forme un graphe 2-régulier connecté sur tous les sommets, avec la connexité exprimée comme ci-dessus et la 2-régularité exprimée comme l'incidence de deux mais pas trois arêtes distinctes à chaque sommet. Cependant, cette propriété n'est pas exprimable dans MSO₁, parce que MSO₁ n'est pas capable de distinguer les graphes bipartites complets avec un nombre égal de sommets de chaque côté de la bipartition (qui sont hamiltoniens) des graphes bipartites complets déséquilibrés (qui ne le sont pas).

Bien que cela ne fasse pas partie de la définition de MSO₂, l'orientation des graphes non orientés peuvent être représentés par une technique impliquant des Arbres de Trémaux. Cela permet également d'exprimer d'autres propriétés de graphe impliquant des orientations.

Théorème de Courcelle

Selon le Théorème de Courcelle, toute propriété de MSO₂ peut être testée en temps linéaire sur des graphes dont la largeur arborescente est bornée, et toute propriété de MSO₁ peut être testée en temps linéaire sur des graphes dont la largeur de clique est bornée. Ce résultat pour les graphes de largeur arborescente bornée garanti aussi l'existence d'un algorithme LOG-SPACE. Une application de ce résultat est le développement d'un algorithme permettant de calculer le nombre de croisement d'un graphe en un temps raisonnable.

Théorème de Seese

Le problème de satisfaisabilité pour une proposition de la logique monadique du second ordre, est le problème de déterminer s'il existe au moins un graphe (éventuellement dans une famille restreinte de graphes) pour lequel la proposition est vraie. Sans restriction, ce problème est indécidable. Cependant, la satisfaisabilité des propositions de MSO₂ décidable pour les graphes de largeur arborescente bornée et de satisfaisabilité des propositions MSO₁ est décidable pour les graphes de largeur de clique bornée. La preuve repose sur le théorème de Courcelle pour construire un automate capable de tester la propriété, puis à examiner l'automate pour déterminer s'il existe un graphe qu'il peut accepter. L'inverse est partiellement vraie, Seese (1991) a prouvé que, lorsqu'une famille de graphes est décidable pour MSO₂, cette famille doit avoir une largeur arborescente bornée. Seese a également conjecturé que chaque famille de graphes décidable pour MSO₁ doit avoir une largeur de clique bornée. Cela n'a toutefois été prouvé, que dans une version faible autorisant les prédicats de comptage modulaires.

Notes et références

Bibliographie

• (en) H. J. Sander Bruggink et Barbara König, « Recognizable languages of arrows and cospans », Mathematical Structures in Computer Science, vol. 28,‎ 2018, p. 1290–1332 (DOI 10.1017/S096012951800018X, S2CID 52275704).
• (en) Jin-Yi Cai, Martin Fürer et Neil Immerman, « An optimal lower bound on the number of variables for graph identification », Combinatorica, vol. 12,‎ 1992, p. 389–410 (DOI 10.1007/BF01305232).
• (en) Jianer Chen, Xiuzhen Huang, Iyad A. Kanj et Ge Xia, « Strong computational lower bounds via parameterized complexity », Journal of Computer and System Sciences, vol. 72,‎ 2006, p. 1346–1367 (DOI 10.1016/j.jcss.2006.04.007 ).
• (en) Bruno Courcelle, « On the expression of graph properties in some fragments of monadic second-order logic », dans Proc. Descr. Complex. Finite Models, vol. 31, Amer. Math. Soc., 1996, 33–62 p. (lire en ligne).
• (en) Bruno Courcelle et Joost Engelfriet, Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, vol. 138, Cambridge University Press, coll. « Encyclopedia of Mathematics and its Applications », 2012 (ISBN 9781139644006, zbMATH 1257.68006).
• (en) Bruno Courcelle, « Fly-automata for checking MSO₂ graph properties », Discrete Applied Mathematics, vol. 245,‎ 2018, p. 236–252 (DOI 10.1016/j.dam.2016.10.018).
• (en) Bruno Courcelle et Sang-il Oum, « Vertex-minors, monadic second-order logic, and a conjecture by Seese », Journal of Combinatorial Theory, vol. 97,‎ 2007, p. 91–126 (DOI 10.1016/j.jctb.2006.04.003 , lire en ligne).
• R. G. Downey et M. R. Fellows, « Fixed-parameter tractability and completeness. II. On completeness for W[1] », Theoretical Computer Science, vol. 141,‎ 1995, p. 109–131 (DOI 10.1016/0304-3975(94)00097-3 ).
• (en) Zdeněk Dvořák, Daniel Kráľ et Robin Thomas, « Deciding first-order properties for sparse graphs », dans Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), 2010, 133–142 p. (ISBN 978-0-7695-4244-7, DOI 10.1109/FOCS.2010.20, MR 3024787, S2CID 15264036, CiteSeer^x 10.1.1.170.9781).
• (en) Michael Elberfeld, Andreas Jakoby et Till Tantau, « Logspace Versions of the Theorems of Bodlaender and Courcelle », dans Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), octobre 2010, 143–152 p. (DOI 10.1109/FOCS.2010.21, S2CID 1820251, lire en ligne [PDF]).
• (en) Ronald Fagin, « Probabilities on finite models », Journal of Symbolic Logic, vol. 41,‎ 1976, p. 50–58 (DOI 10.1017/s0022481200051756, JSTOR 2272945, MR 0476480, S2CID 2563318, lire en ligne).
• (en) Ronald Fagin, Larry J. Stockmeyer et Moshe Y. Vardi, « On monadic NP vs monadic co-NP », Information and Computation, vol. 120,‎ 1995, p. 78–92 (DOI 10.1006/inco.1995.1100 , MR 1340807).
• (en) Ju. V. Glebskiĭ, D. I. Kogan, M. I. Liogon'kiĭ et V. A. Talanov, « Volume and fraction of satisfiability of formulas of the lower predicate calculus », Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika,‎ 1969, p. 17–27 (MR 0300882).
• (en) Leslie Ann Goldberg, « Polynomial space polynomial delay algorithms for listing families of graphs », dans Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing (STOC '93), New York, NY, USA, ACM, 1993, 218–225 p. (ISBN 0-89791-591-7, DOI 10.1145/167088.167160, S2CID 6305108).
• (en) Étienne Grandjean, « Complexity of the first-order theory of almost all finite structures », Information and Control, vol. 57,‎ 1983, p. 180–204 (DOI 10.1016/S0019-9958(83)80043-6 , MR 742707)
• (en) Martin Grohe, « Computing crossing numbers in quadratic time », dans Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing (STOC '01), 2001, 231–236 p. (DOI 10.1145/380752.380805, arXiv cs/0009010, S2CID 724544)
• (en) Martin Grohe, Descriptive complexity, canonisation, and definable graph structure theory, vol. 47, Cambridge University Press, Cambridge, coll. « Lecture Notes in Logic », 2017 (ISBN 978-1-107-01452-7, MR 3729479)
• (en) Martin Grohe, Stephan Kreutzer et Sebastian Siebertz, « Deciding first-order properties of nowhere dense graphs », dans Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC '14), New York, ACM, 2014, 89–98 p. (ISBN 978-1-4503-2710-7, DOI 10.1145/2591796.2591851, arXiv 1311.3899, S2CID 13297133)
• (en) Lauri Hella, Phokion G. Kolaitis et Kerkko Luosto, « Almost everywhere equivalence of logics in finite model theory », The Bulletin of Symbolic Logic, vol. 2,‎ 1996, p. 422–443 (DOI 10.2307/421173, JSTOR 421173, MR 1460316, S2CID 16411368)
• (en) C. Ward Henson, « Countable homogeneous relational structures and $\aleph _{0}$-categorical theories », The Journal of Symbolic Logic, vol. 37,‎ 1972, p. 494–500 (DOI 10.2307/2272734, JSTOR 2272734, MR 321727, S2CID 40662635)
• (en) Neil Immerman et Eric Lander, « Describing graphs: a first-order approach to graph canonization », dans Complexity Theory Retrospective: In honor of Juris Hartmanis on the occasion of his sixtieth birthday, New York, Springer-Verlag, 1990, 59–81 p. (DOI 10.1007/978-1-4612-4478-3_5, MR 1060782)
• (en) I. A. Lavrov, « The effective non-separability of the set of identically true formulae and the set of finitely refutable formulae for certain elementary theories », Algebra i Logika Sem., vol. 2,‎ 1963, p. 5–18 (MR 0157904).
• (en) Ken-ichi Kawarabayashi et Bruce Reed, « Computing crossing number in linear time », dans Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC '07), 2007, 382–390 p. (DOI 10.1145/1250790.1250848, S2CID 13000831).
• (en) Leszek Koncewicz, « Definability of classes of graphs in the first order predicate calculus with identity », Polish Academy of Sciences, vol. 32,‎ 1973, p. 159–190 (DOI 10.1007/BF02123839, JSTOR 20014678, MR 351796, S2CID 189786935).
• (en) Bastian Laubner, « Capturing polynomial time on interval graphs », dans 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Los Alamitos, California, IEEE Computer Society, 2010, 199–208 p. (DOI 10.1109/LICS.2010.42, MR 2963094, arXiv 0911.3799, S2CID 1450409).
• (en) Leonid Libkin, Elements of finite model theory, Springer-Verlag, Berlin, coll. « Texts in Theoretical Computer Science: An EATCS Series », 2004 (ISBN 3-540-21202-7, DOI 10.1007/978-3-662-07003-1, MR 2102513, S2CID 30176939, lire en ligne ).
• (en) James F. Lynch, « Probabilities of sentences about very sparse random graphs », Random Structures & Algorithms, vol. 3,‎ 1992, p. 33–53 (DOI 10.1002/rsa.3240030105, MR 1139487).
• (en) Jaroslav Nešetřil et Patrice Ossona de Mendez, Sparsity: Graphs, Structures, and Algorithms, vol. 28, Springer-Verlag, coll. « Algorithms and Combinatorics », 2012 (ISBN 978-3-642-27874-7, DOI 10.1007/978-3-642-27875-4, MR 2920058).
• (en) Paweł Parys, « first-order logic on CPDA graphs », dans Computer science—theory and applications, vol. 8476, New York, Springer-Verlag, coll. « Lecture Notes in Computer Science », 2014, 300–313 p. (DOI 10.1007/978-3-319-06686-8_23, MR 3218557, S2CID 31640587).
• (en) Oleg Pikhurko, Joel Spencer et Oleg Verbitsky, « Succinct definitions in the first order theory of graphs », Annals of Pure and Applied Logic, vol. 139,‎ 2006, p. 74–109 (DOI 10.1016/j.apal.2005.04.003, MR 2206252, arXiv math/0401307, S2CID 3041191).
• (en) Oleg Pikhurko et Oleg Verbitsky, « Logical complexity of graphs: a survey », dans Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, January 5-8, 2009, Washington, DC), vol. 558, American Mathematical Society, coll. « Contemporary Mathematics », 2011, 129–180 p. (ISBN 978-0-8218-8322-8, arXiv 1003.4865).
• (en) D. Seese, « The structure of the models of decidable monadic theories of graphs », Annals of Pure and Applied Logic, vol. 53,‎ 1991, p. 169–195 (DOI 10.1016/0168-0072(91)90054-P , MR 1114848).
• (en) Saharon Shelah et Joel Spencer, « Zero-one laws for sparse random graphs », Journal of the American Mathematical Society, vol. 1,‎ 1988, p. 97–115 (DOI 10.2307/1990968 , JSTOR 1990968, MR 924703).
• (en) Joel Spencer, « Infinite spectra in the first order theory of graphs », Combinatorica, vol. 10,‎ 1990, p. 95–102 (DOI 10.1007/BF02122699, MR 1075070, S2CID 27770505).
• (en) Joel Spencer, The Strange Logic of Random Graphs, vol. 22, Springer-Verlag, Berlin, coll. « Algorithms and Combinatorics », 2001 (ISBN 3-540-41654-4, DOI 10.1007/978-3-662-04538-1).
• (en) B. A. Trahtenbrot, « The impossibility of an algorithm for the decision problem for finite domains », Doklady Akademii Nauk SSSR, vol. 70,‎ 1950, p. 569–572 (MR 0033784).
• (en) Oleg Verbitsky, « The first order definability of graphs with separators via the Ehrenfeucht game », Theoretical Computer Science, vol. 343,‎ 2005, p. 158–176 (DOI 10.1016/j.tcs.2005.05.003, MR 2168849, arXiv math/0401361, S2CID 17886484).
• (en) Oleg Verbitsky et Maksim Zhukovskii, « Tight bounds on the asymptotic descriptive complexity of subgraph isomorphism », ACM Transactions on Computational Logic, vol. 20,‎ 2019, A9:1–A9:18 (DOI 10.1145/3303881, MR 3942556, arXiv 1802.02143, S2CID 3603039).
• (en) Thomas Zeume, « The dynamic descriptive complexity of k-clique », Information and Computation, vol. 256,‎ 2017, p. 9–22 (DOI 10.1016/j.ic.2017.04.005, MR 3705411, S2CID 1412001, lire en ligne).