Logique des graphes

Dans les domaines mathématiques de la théorie des graphes et de la théorie des modèles finis, le logique des graphes traite de la spécification formelle de propriétés de graphe en utilisant des proposition 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 peut être vraie pour certains graphes et fausse pour d'autres; un graphe est un modèle de , écrire , si est vraie sur les sommets et la relation d'adjacence de . 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. vignette|Le graphique illustré ici apparaît comme le sous-graphe d'un graphe non orienté si et seulement si modélise la proposition .