Théorème de CourcelleEn algorithmique et en théorie de la complexité, le théorème de Courcelle est le suivant : C'est un métathéorème, dans le sens où il concerne une classe de problèmes algorithmiques. Le théorème est dû à Bruno Courcelle. Dans le contexte de ce théorème, un graphe est donné par un ensemble de sommets et une relation d'adjacence , et la restriction à la logique monadique signifie que la propriété étudiée peut contenir des quantificateurs sur des ensembles de sommets (quantificateurs du second ordre sur des prédicats monadiques), mais pas de quantificateurs sur des ensembles d'arcs (ces quantificateurs du second ordre porteraient sur des prédicats binaires).
Logique monadique du second ordrevignette|En logique monadique du second ordre, il y a des variables du premier ordre (x, y, etc.) qui représentent des éléments du domaine et des variables du second ordre (A, Z, etc.) qui représentent des sous-ensembles d'éléments. En logique mathématique et en informatique théorique, la logique monadique du second ordre (abrégé en MSO pour monadic second order) est l'extension de la logique du premier ordre avec des variables dénotant des ensembles.
Vérification de modèlesthumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.
Forbidden graph characterizationIn graph theory, a branch of mathematics, many important families of graphs can be described by a finite set of individual graphs that do not belong to the family and further exclude all graphs from the family which contain any of these forbidden graphs as (induced) subgraph or minor. A prototypical example of this phenomenon is Kuratowski's theorem, which states that a graph is planar (can be drawn without crossings in the plane) if and only if it does not contain either of two forbidden graphs, the complete graph K_5 and the complete bipartite graph K_3,3.
Largeur arborescenteEn théorie des graphes et en informatique théorique, la largeur arborescente ou largeur d'arbre d'un graphe (treewidth en anglais) est un nombre qui, intuitivement, mesure s'il est proche d'un arbre. Elle peut être définie de plusieurs manières, notamment en utilisant la décomposition arborescente. Souvent, un problème algorithmique facile sur les arbres est en fait facile pour les graphes qui ressemblent à des arbres. Ainsi, ce paramètre est souvent utilisé en algorithmique de graphes, notamment pour les schémas d'approximation polynomiaux et complexité paramétrée.
