Logic of graphs

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using logical formulas. There are several variations in the types of logical operation that can be used in these formulas. The first order logic of graphs concerns formulas in which the variables and predicates concern individual vertices and edges of a graph, while monadic second order graph logic allows quantification over sets of vertices or edges.

A sentence ${\displaystyle S}$ may be true for some graphs, and false for others; a graph ${\displaystyle G}$ is said to model ${\displaystyle S}$, written ${\displaystyle G\models S}$, if ${\displaystyle S}$ is true of the vertices and adjacency relation of ${\displaystyle G}$. The algorithmic problem of model checking concerns testing whether a given graph models a given sentence. The algorithmic problem of satisfiability concerns testing whether there exists a graph that models a given sentence. Although both model checking and satisfiability are hard in general, several major algorithmic meta-theorems show that properties expressed in this way can be tested efficiently for important classes of graphs.

...
Wikipedia