Logic of graphs

<h2 id="first-order">First order</h2>

In the <a href="/facts/First-order_logic/lcISqWIg">first-order logic</a> of graphs, a graph property is expressed as a quantified logical sentence whose variables represent graph <a href="/facts/Vertex_(graph_theory)/WhlWmL3o">vertices</a>, with <a href="/facts/Predicate_(mathematical_logic)/5WazAvKF">predicates</a> for equality and adjacency testing.<a class="footnote-ref" id="fnref:1" href="#fn:1">1</a>

<h3>Examples</h3>
For instance, the condition that a graph does not have any <a href="/facts/Isolated_vertex/WhlWmL3o">isolated vertices</a> may be expressed by the sentence

∀
        u
        ∃
        v
        (
        u
        ∼
        v
        )
      
    
    {\displaystyle \forall u\exists v(u\sim v)}

where the 
 
 
 
 ∼
 
 
 {\displaystyle \sim }
 
 symbol indicates the undirected adjacency relation between two vertices. This sentence can be interpreted as meaning that for every vertex 
 
 
 
 u
 
 
 {\displaystyle u}
 
 there is another vertex 
 
 
 
 v
 
 
 {\displaystyle v}
 
 that is adjacent to 
 
 
 
 u
 
 
 {\displaystyle u}
 
.<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a>
The <a href="/facts/Subgraph_isomorphism_problem/86LLWRg4">subgraph isomorphism problem</a> for a fixed subgraph 
 
 
 
 H
 
 
 {\displaystyle H}
 
 asks whether 
 
 
 
 H
 
 
 {\displaystyle H}
 
 appears as a subgraph of a larger graph 
 
 
 
 G
 
 
 {\displaystyle G}
 
. It may be expressed by a sentence that states the existence of vertices (one for each vertex of 
 
 
 
 H
 
 
 {\displaystyle H}
 
) such that, for each edge of 
 
 
 
 H
 
 
 {\displaystyle H}
 
, the corresponding pair of variables represent adjacent vertices and such that, for each remaining pair of vertices of 
 
 
 
 H
 
 
 {\displaystyle H}
 
, the corresponding pair of variables represent distinct vertices;<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a> see the illustration. As a special case, the <a href="/facts/Clique_problem/cVVBNP08">clique problem</a> (for a fixed clique size) may be expressed by a sentence that states the existence of a number of vertices equal to the clique size, all of which are adjacent.<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a>

<h3>Axioms</h3>
For simple <a href="/facts/Undirected_graph/kw3eIBUe">undirected graphs</a>, the first-order theory of graphs includes the <a href="/facts/Axiom/mLjP14Mc">axioms</a>

∀
 u
 
 
 (
 
 
 ¬
 (
 u
 ∼
 u
 )
 
 
 )
 
 
 
 
 {\displaystyle \forall u{\bigl (}\lnot (u\sim u){\bigr )}}
 
 (the graph cannot contain any <a href="/facts/Loop_(graph_theory)/jCuevIad">loops</a>), and

∀
 u
 ∀
 v
 (
 u
 ∼
 v
 ⇒
 v
 ∼
 u
 )
 
 
 {\displaystyle \forall u\forall v(u\sim v\Rightarrow v\sim u)}
 
 (edges are undirected).<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a>
Other types of graphs, such as <a href="/facts/Directed_graph/YBdfQ0um">directed graphs</a>, may involve different axioms,<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a> and logical formulations of <a href="/facts/Multigraph/udmS0Cp0">multigraph</a> properties require special handling such as having multiple edge relations<a class="footnote-ref" id="fnref:7" href="#fn:7">7</a> or separate variables for vertices and edges.<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a>

<h3>Zero-one law</h3>

Glebskiĭ et al. (1969) and, independently,
Fagin (1976) proved a <a href="/facts/Zero%25E2%2580%2593one_law/rPknLnda">zero–one law</a> for first-order graph logic; Fagin's proof used the <a href="/facts/Compactness_theorem/8tHVkdeK">compactness theorem</a>. According to this result, every first-order sentence is either <a href="/facts/Almost_always/fWaxzpBA">almost always</a> true or almost always false for <a href="/facts/Random_graph/gfQhq1Sz">random graphs</a> in the <a href="/facts/Erd%25C5%2591s%25E2%2580%2593R%25C3%25A9nyi_model/F6BQ8gIj">Erdős–Rényi model</a>. That is, let 
 
 
 
 S
 
 
 {\displaystyle S}
 
 be a fixed first-order sentence, and choose a random 
 
 
 
 n
 
 
 {\displaystyle n}
 
-vertex graph 
 
 
 
 
 G
 
 n
 
 
 
 
 {\displaystyle G_{n}}
 
 uniformly at random among all graphs on a set of 
 
 
 
 n
 
 
 {\displaystyle n}
 
 labeled vertices. Then in the limit as 
 
 
 
 n
 
 
 {\displaystyle n}
 
 tends to infinity the probability that 
 
 
 
 
 G
 
 n
 
 
 
 
 {\displaystyle G_{n}}
 
 models 
 
 
 
 S
 
 
 {\displaystyle S}
 
 will tend either to zero or to one:

lim
          
            n
            →
            ∞
          
        
        Pr
        ⁡
        [
        
          G
          
            n
          
        
        ⊨
        S
        ]
        ∈
        {
        0
        ,
        1
        }
        .
      
    
    {\displaystyle \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]\in \{0,1\}.}

Moreover, there is a specific infinite graph, the <a href="/facts/Rado_graph/dbPjeUoB">Rado graph</a> 
 
 
 
 R
 
 
 {\displaystyle R}
 
, such that the sentences modeled by the Rado graph are exactly the ones for which the probability of being modeled by a random finite graph tends to one:

R
        ⊨
        S
        
        ⟺
        
        
          lim
          
            n
            →
            ∞
          
        
        Pr
        ⁡
        [
        
          G
          
            n
          
        
        ⊨
        S
        ]
        =
        1.
      
    
    {\displaystyle R\models S\quad \Longleftrightarrow \quad \lim _{n\to \infty }\operatorname {Pr} [G_{n}\models S]=1.}

For random graphs in which each edge is included independently of the others with a fixed probability, the same result is true, with the same sentences having probabilities tending to zero or to one.<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a>
The <a href="/facts/Computational_complexity_theory/etHuVF3U">computational complexity</a> of determining whether a given sentence has probability tending to zero or to one is high: the problem is <a href="/facts/PSPACE-complete/gkV3vHfX">PSPACE-complete</a>.<a class="footnote-ref" id="fnref:10" href="#fn:10">10</a>
If a first-order graph property has probability tending to one on random graphs, then it is possible to list all the 
 
 
 
 n
 
 
 {\displaystyle n}
 
-vertex graphs that model the property, with <a href="/facts/Polynomial_delay/FfNjhNM2">polynomial delay</a> (as a function of 
 
 
 
 n
 
 
 {\displaystyle n}
 
) per graph.<a class="footnote-ref" id="fnref:11" href="#fn:11">11</a>
A similar analysis can be performed for non-uniform random graphs, where the probability of including an edge is a function of the number of vertices, and where the decision to include or exclude an edge is made independently with equal probability for all edges. However, for these graphs the situation is more complicated.
In this case, a first-order property may have one or more thresholds, such that when the edge <a href="/facts/Inclusion_probability/Vob3umvl">inclusion probability</a> is bounded away from the threshold then the probability of having the given property tends to zero or one. These thresholds can never be an irrational power of 
 
 
 
 n
 
 
 {\displaystyle n}
 
, so random graphs where the edge inclusion probability is an irrational power obey a zero-one law analogous to the one for uniformly random graphs. A similar zero-one law holds for very sparse random graphs that have an edge inclusion probability of 
 
 
 
 
 n
 
 −
 c
 
 
 
 
 {\displaystyle n^{-c}}
 
 with 
 
 
 
 c
 >
 1
 
 
 {\displaystyle c>1}
 
, as long as 
 
 
 
 c
 
 
 {\displaystyle c}
 
 is not a <a href="/facts/Superparticular_ratio/4bs1NrAV">superparticular ratio</a>.<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a> If 
 
 
 
 c
 
 
 {\displaystyle c}
 
 is superparticular, the probability of having a given property may tend to a limit that is not zero or one, but this limit can be calculated efficiently.<a class="footnote-ref" id="fnref:13" href="#fn:13">13</a> There exist first-order sentences that have infinitely many thresholds.<a class="footnote-ref" id="fnref:14" href="#fn:14">14</a>

<h3>Parameterized complexity</h3>
If a first-order sentence includes 
 
 
 
 k
 
 
 {\displaystyle k}
 
 distinct variables, then the property it describes can be tested in graphs of 
 
 
 
 n
 
 
 {\displaystyle n}
 
 vertices by examining all 
 
 
 
 k
 
 
 {\displaystyle k}
 
-tuples of vertices; however, this <a href="/facts/Brute_force_search/YU2fzBIt">brute force search</a> algorithm is not particularly efficient, taking time 
 
 
 
 O
 (
 
 n
 
 k
 
 
 )
 
 
 {\displaystyle O(n^{k})}
 
.
The problem of checking whether a graph models a given first-order sentence includes as special cases the <a href="/facts/Subgraph_isomorphism_problem/86LLWRg4">subgraph isomorphism problem</a> (in which the sentence describes the graphs that contain a fixed subgraph) and the <a href="/facts/Clique_problem/cVVBNP08">clique problem</a> (in which the sentence describes graphs that contain complete subgraphs of a fixed size).
The clique problem is hard for <a href="/facts/W(1)/RoyaJGgJ">W(1)</a>, the first level of a hierarchy of hard problems from the point of view of <a href="/facts/Parameterized_complexity/RoyaJGgJ">parameterized complexity</a>. Therefore, it is unlikely to have a fixed-parameter tractable algorithm, one whose running time takes the form 
 
 
 
 O
 (
 f
 (
 k
 )
 
 n
 
 c
 
 
 )
 
 
 {\displaystyle O(f(k)n^{c})}
 
 for a function 
 
 
 
 f
 
 
 {\displaystyle f}
 
 and constant 
 
 
 
 c
 
 
 {\displaystyle c}
 
 that are independent of 
 
 
 
 k
 
 
 {\displaystyle k}
 
 and 
 
 
 
 n
 
 
 {\displaystyle n}
 
.<a class="footnote-ref" id="fnref:15" href="#fn:15">15</a>
More strongly, if the <a href="/facts/Exponential_time_hypothesis/DpxBBNVK">exponential time hypothesis</a> is true, then clique-finding and first-order model checking would necessarily take time proportional to a power of 
 
 
 
 n
 
 
 {\displaystyle n}
 
 whose exponent is proportional to 
 
 
 
 k
 
 
 {\displaystyle k}
 
.<a class="footnote-ref" id="fnref:16" href="#fn:16">16</a>
On restricted classes of graphs, model checking of first-order sentences can be much more efficient. In particular, every graph property expressible as a first-order sentence can be tested in <a href="/facts/Linear_time/77T62gmf">linear time</a> for the graphs of <a href="/facts/Bounded_expansion/9Dv8GYp9">bounded expansion</a>. These are the graphs in which all <a href="/facts/Shallow_minor/YS9HTlDL">shallow minors</a> are <a href="/facts/Sparse_graph/xFC7b7s9">sparse graphs</a>, with a ratio of edges to vertices bounded by a function of the depth of the minor. Even more generally, first-order model checking can be performed in near-linear time for nowhere-dense graphs, classes of graphs for which, at each possible depth, there is at least one forbidden shallow minor. Conversely, if model checking is fixed-parameter tractable for any monotone family of graphs, that family must be nowhere-dense.<a class="footnote-ref" id="fnref:17" href="#fn:17">17</a>

<h3>Data compression and graph isomorphism</h3>
A first-order sentence 
 
 
 
 S
 
 
 {\displaystyle S}
 
 in the logic of graphs is said to define a graph 
 
 
 
 G
 
 
 {\displaystyle G}
 
 if 
 
 
 
 G
 
 
 {\displaystyle G}
 
 is the only graph that models 
 
 
 
 S
 
 
 {\displaystyle S}
 
. Every graph may be defined by at least one sentence; for instance, one can define any 
 
 
 
 n
 
 
 {\displaystyle n}
 
-vertex graph 
 
 
 
 G
 
 
 {\displaystyle G}
 
 by a sentence with 
 
 
 
 n
 +
 1
 
 
 {\displaystyle n+1}
 
 variables, one for each vertex of the graph, and one more to state the condition that there is no vertex other than the 
 
 
 
 n
 
 
 {\displaystyle n}
 
 vertices of the graph. Additional clauses of the sentence can be used to ensure that no two vertex variables are equal, that each edge of 
 
 
 
 G
 
 
 {\displaystyle G}
 
 is present, and no edge exists between a pair of non-adjacent vertices of 
 
 
 
 G
 
 
 {\displaystyle G}
 
. However, for some graphs there exist significantly shorter sentences that define the graph.<a class="footnote-ref" id="fnref:18" href="#fn:18">18</a>
Several different <a href="/facts/Graph_invariant/bjuIvgb1">graph invariants</a> can be defined from the simplest sentences (with different measures of simplicity) that define a given graph. In particular the logical depth of a graph is defined to be the minimum level of nesting of quantifiers (the <a href="/facts/Quantifier_rank/GzQNst0v">quantifier rank</a>) in a sentence defining the graph.<a class="footnote-ref" id="fnref:19" href="#fn:19">19</a> The sentence outlined above nests the quantifiers for all of its variables, so it has logical depth 
 
 
 
 n
 +
 1
 
 
 {\displaystyle n+1}
 
. The logical width of a graph is the minimum number of variables in a sentence that defines it.<a class="footnote-ref" id="fnref:20" href="#fn:20">20</a> In the sentence outlined above, this number of variables is again 
 
 
 
 n
 +
 1
 
 
 {\displaystyle n+1}
 
. Both the logical depth and logical width can be bounded in terms of the <a href="/facts/Treewidth/uoITxzRJ">treewidth</a> of the given graph.<a class="footnote-ref" id="fnref:21" href="#fn:21">21</a> The logical length, analogously, is defined as the length of the shortest sentence describing the graph. The sentence described above has length proportional to the square of the number of vertices, but it is possible to define any graph by a sentence with length proportional to its number of edges.<a class="footnote-ref" id="fnref:22" href="#fn:22">22</a>
All trees, and most graphs, can be described by first-order sentences with only two variables, but extended by counting predicates. For graphs that can be described by sentences in this logic with a fixed constant number of variables, it is possible to find a <a href="/facts/Graph_canonization/KfmqQ0sG">graph canonization</a> in polynomial time (with the exponent of the polynomial equal to the number of variables). By comparing canonizations, it is possible to solve the <a href="/facts/Graph_isomorphism_problem/Buhk3qsS">graph isomorphism problem</a> for these graphs in polynomial time.<a class="footnote-ref" id="fnref:23" href="#fn:23">23</a>

<h3>Satisfiability</h3>
As a special case of <a href="/facts/Trakhtenbrot%2527s_theorem/Xjz7VWd4">Trakhtenbrot's theorem</a>, it is <a href="/facts/Undecidable_problem/QBxmXBbY">undecidable</a> whether a given first-order sentence can be realized by a finite undirected graph. This means that no algorithm can correctly answer this question for all sentences.<a class="footnote-ref" id="fnref:24" href="#fn:24">24</a>
Some first-order sentences are modeled by infinite graphs but not by any finite graph. For instance, the property of having exactly one vertex of <a href="/facts/Degree_(graph_theory)/LnFFpI8v">degree</a> one, with all other vertices having degree exactly two, can be expressed by a first-order sentence. It is modeled by an infinite <a href="/facts/End_(graph_theory)/l5B9xEQz">ray</a>, but violates Euler's <a href="/facts/Handshaking_lemma/z51Dg4R5">handshaking lemma</a> for finite graphs. However, it follows from the negative solution to the <a href="/facts/Entscheidungsproblem/y8LDal2X">Entscheidungsproblem</a> (by <a href="/facts/Alonzo_Church/b7D52Itv">Alonzo Church</a> and <a href="/facts/Alan_Turing/klov9b6g">Alan Turing</a> in the 1930s) that satisfiability of first-order sentences for graphs that are not constrained to be finite remains undecidable. It is also undecidable to distinguish between the first-order sentences that are true for all graphs and the ones that are true of finite graphs but false for some infinite graphs.<a class="footnote-ref" id="fnref:25" href="#fn:25">25</a>

<h2 id="fixed-point">Fixed point</h2>

<a href="/facts/Least_fixed_point/JbcBLqTN">Least fixed point</a> based logics of graphs extend the first-order logic of graphs by allowing predicates (properties of vertices or tuples of vertices) defined by special fixed-point operators. This kind of definition begins with an implication, a formula stating that when certain values of the predicate are true, then other values are true as well. A "fixed point" is any predicate for which this is a valid implication. There may be many fixed points, including the always-true predicate; a "least fixed point" is a fixed point that has as few true values as possible. More precisely, its true values should be a subset of the true values of any other fixed point.<a class="footnote-ref" id="fnref:26" href="#fn:26">26</a>
For instance, define 
 
 
 
 C
 (
 u
 ,
 v
 )
 
 
 {\displaystyle C(u,v)}
 
 to be true when the two vertices 
 
 
 
 u
 
 
 {\displaystyle u}
 
 and 
 
 
 
 v
 
 
 {\displaystyle v}
 
 are connected by a path in a given graph, and false otherwise.
Then every vertex is connected to itself, and when 
 
 
 
 u
 
 
 {\displaystyle u}
 
 is connected to a neighbor of 
 
 
 
 v
 
 
 {\displaystyle v}
 
, it is also connected by one more step to 
 
 
 
 v
 
 
 {\displaystyle v}
 
. Expressing this reasoning in logical terms, 
 
 
 
 C
 
 
 {\displaystyle C}
 
 is the least fixed point of the formula

C
        (
        u
        ,
        v
        )
        ←
        
          
            (
          
        
        (
        u
        =
        v
        )
        ∨
        ∃
        w
        
          
            (
          
        
        C
        (
        u
        ,
        w
        )
        ∧
        w
        ∼
        v
        
          
            )
          
        
        
          
            )
          
        
        .
      
    
    {\displaystyle C(u,v)\leftarrow {\Bigl (}(u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.}

Here, being a fixed point means that the truth of the right side of the formula implies the truth of the left side, as the reversed implication arrow suggests. Being the least fixed point, in this case, implies that no two vertices will be defined as connected unless their connectivity comes from repeated use of this implication.<a class="footnote-ref" id="fnref:27" href="#fn:27">27</a>
Several variations of fixed point logics have been studied. In least fixed point logic, the right hand side of the 
 
 
 
 ←
 
 
 {\displaystyle \leftarrow }
 
 operator in the defining formula must use the predicate only positively (that is, each appearance should be nested within an even number of negations) in order to make the least fixed point well defined.
In another variant with equivalent logical power, inflationary fixed point logic, the formula need not be monotone but the resulting fixed point is defined as the one obtained by repeatedly applying implications derived from the defining formula starting from the all-false predicate.
Other variants, allowing negative implications or multiple simultaneously-defined predicates, are also possible, but provide no additional definitional power.
A predicate, defined in one of these ways, can then be applied to a tuple of vertices as part of a larger logical sentence.<a class="footnote-ref" id="fnref:28" href="#fn:28">28</a>
Fixed point logics, and extensions of these logics that also allow integer counting variables whose values range from 0 to the number of vertices, have been used in <a href="/facts/Descriptive_complexity/Ec5F9CnT">descriptive complexity</a> in an attempt to provide a logical description of <a href="/facts/Decision_problem/cQNWjbdE">decision problems</a> in graph theory that can be decided in <a href="/facts/Polynomial_time/77T62gmf">polynomial time</a>. The fixed point of a logical formula can be constructed in polynomial time, by an algorithm that repeatedly adds tuples to the set of values for which the predicate is true until reaching a fixed point, so deciding whether a graph models a sentence in this logic can always be decided in polynomial time. Not every polynomial time graph property can be modeled by a sentence in a logic that uses only fixed points and counting.<a class="footnote-ref" id="fnref:29" href="#fn:29">29</a><a class="footnote-ref" id="fnref:30" href="#fn:30">30</a> However, for some special classes of graphs the polynomial time properties are the same as the properties expressible in fixed point logic with counting. These include random graphs,<a class="footnote-ref" id="fnref:31" href="#fn:31">31</a><a class="footnote-ref" id="fnref:32" href="#fn:32">32</a> <a href="/facts/Interval_graph/oLwYI3uT">interval graphs</a>,<a class="footnote-ref" id="fnref:33" href="#fn:33">33</a><a class="footnote-ref" id="fnref:34" href="#fn:34">34</a> and (through a logical expression of the <a href="/facts/Graph_structure_theorem/tN6y8cAY">graph structure theorem</a>) every class of graphs characterized by <a href="/facts/Forbidden_minor/50Kex6JU">forbidden minors</a>.<a class="footnote-ref" id="fnref:35" href="#fn:35">35</a>

<h2 id="second-order">Second order</h2>
In the <a href="/facts/Monadic_second-order_logic/m9g3W9VP">monadic second-order logic</a> of graphs, the variables represent objects of up to four types: vertices, edges, sets of vertices, and sets of edges. There are two main variations of monadic second-order graph logic: MSO1 in which only vertex and vertex set variables are allowed, and MSO2 in which all four types of variables are allowed. The predicates on these variables include equality testing, membership testing, and either vertex-edge incidence (if both vertex and edge variables are allowed) or adjacency between pairs of vertices (if only vertex variables are allowed). Additional variations in the definition allow additional predicates such as modular counting predicates.<a class="footnote-ref" id="fnref:36" href="#fn:36">36</a>

<h3>Examples</h3>
As an example, the <a href="/facts/Graph_connectivity/FSNjsYhz">connectivity</a> of an undirected graph can be expressed in MSO1 as the statement that, for every partition of the vertices into two nonempty subsets, there exists an edge from one subset to the other. A partition of the vertices can be described by the subset 
 
 
 
 S
 
 
 {\displaystyle S}
 
 of vertices on one side of the partition, and each such subset should either describe a trivial partition (one in which one or the other side is empty) or be crossed by an edge. That is, a graph is connected when it models the MSO1 sentence

∀
        S
        
          
            (
          
        
        ∀
        x
        (
        x
        ∈
        S
        )
        ∨
        ∀
        y
        
          
            (
          
        
        ¬
        (
        y
        ∈
        S
        )
        
          
            )
          
        
        ∨
        ∃
        x
        ∃
        y
        
          
            (
          
        
        x
        ∈
        S
        ∧
        ¬
        (
        y
        ∈
        S
        )
        ∧
        x
        ∼
        y
        
          
            )
          
        
        
          
            )
          
        
        .
      
    
    {\displaystyle \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 )}.}

However, connectivity cannot be expressed in first-order graph logic, nor can it be expressed in existential MSO1 (the <a href="/facts/Fragment_(logic)/KxvnWnl9">fragment</a> of MSO1 in which all set quantifiers are existential and occur at the beginning of the sentence) nor even existential MSO2.<a class="footnote-ref" id="fnref:37" href="#fn:37">37</a>
<a href="/facts/Hamiltonian_path/MHjY2xoY">Hamiltonicity</a> can be expressed in MSO2 by the existence of a set of edges that forms a connected 2-regular graph on all the vertices, with connectivity expressed as above and 2-regularity expressed as the incidence of two but not three distinct edges at each vertex. However, Hamiltonicity is not expressible in MSO1, because MSO1 is not capable of distinguishing <a href="/facts/Complete_bipartite_graph/C1RYIdpX">complete bipartite graphs</a> with equal numbers of vertices on each side of the bipartition (which are Hamiltonian) from unbalanced complete bipartite graphs (which are not).<a class="footnote-ref" id="fnref:38" href="#fn:38">38</a>
Although not part of the definition of MSO2, <a href="/facts/Orientation_(graph_theory)/GV2KdNtn">orientations</a> of undirected graphs can be represented by a technique involving <a href="/facts/Tr%25C3%25A9maux_tree/T0uFMTHt">Trémaux trees</a>. This allows other graph properties involving orientations to be expressed as well.<a class="footnote-ref" id="fnref:39" href="#fn:39">39</a>

<h3>Courcelle's theorem</h3>
According to <a href="/facts/Courcelle%2527s_theorem/Yy83uBvh">Courcelle's theorem</a>, every fixed MSO2 property can be tested in linear time on graphs of bounded <a href="/facts/Treewidth/uoITxzRJ">treewidth</a>, and every fixed MSO1 property can be tested in linear time on graphs of bounded <a href="/facts/Clique-width/gUJQjevm">clique-width</a>.<a class="footnote-ref" id="fnref:40" href="#fn:40">40</a> The version of this result for graphs of bounded treewidth can also be implemented in <a href="/facts/Logarithmic_space/vCMV0edS">logarithmic space</a>.<a class="footnote-ref" id="fnref:41" href="#fn:41">41</a> Applications of this result include a fixed-parameter tractable algorithm for computing the <a href="/facts/Crossing_number_(graph_theory)/x3Yz6UhF">crossing number</a> of a graph.<a class="footnote-ref" id="fnref:42" href="#fn:42">42</a>

<h3>Seese's theorem</h3>
The <a href="/facts/Satisfiability_problem/NkmQFgHB">satisfiability problem</a> for a sentence of monadic second-order logic is the problem of determining whether there exists at least one graph (possibly within a restricted family of graphs) for which the sentence is true. For arbitrary graph families, and arbitrary sentences, this problem is <a href="/facts/Undecidable_problem/QBxmXBbY">undecidable</a>. However, satisfiability of MSO2 sentences is decidable for the graphs of bounded treewidth, and satisfiability of MSO1 sentences is decidable for graphs of bounded clique-width. The proof involves using Courcelle's theorem to build an automaton that can test the property, and then examining the automaton to determine whether there is any graph it can accept. As a partial converse,<a class="footnote-ref" id="fnref:43" href="#fn:43">43</a> Seese (1991) proved that, whenever a family of graphs has a decidable MSO2 satisfiability problem, the family must have bounded treewidth. The proof is based on a theorem of Robertson and Seymour that the families of graphs with unbounded treewidth have arbitrarily large <a href="/facts/Grid_graph/4EHMt1b6">grid</a> <a href="/facts/Graph_minor/qn5eI22T">minors</a>. Seese also conjectured that every family of graphs with a decidable MSO1 satisfiability problem must have bounded clique-width.<a class="footnote-ref" id="fnref:44" href="#fn:44">44</a> This has not been proven, but a weakening of the conjecture that extends MSO1 with modular counting predicates is true.<a class="footnote-ref" id="fnref:45" href="#fn:45">45</a>

<h2 id="notes">Notes</h2>

<ul><li>Bruggink, H. J. Sander; König, Barbara (2018), "Recognizable languages of arrows and cospans", Mathematical Structures in Computer Science, 28 (8): 1290–1332, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1017%2FS096012951800018X">10.1017/S096012951800018X</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3849613">3849613</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:52275704">52275704</a></li>
<li>Cai, Jin-Yi; Fürer, Martin; <a href="/facts/Neil_Immerman/7aCupltL">Immerman, Neil</a> (1992), "An optimal lower bound on the number of variables for graph identification", <a href="/facts/Combinatorica/AxdqUqrp">Combinatorica</a>, 12 (4): 389–410, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2FBF01305232">10.1007/BF01305232</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1194730">1194730</a></li>
<li>Chen, Jianer; Huang, Xiuzhen; Kanj, Iyad A.; Xia, Ge (2006), "Strong computational lower bounds via parameterized complexity", <a href="/facts/Journal_of_Computer_and_System_Sciences/cNek9ego">Journal of Computer and System Sciences</a>, 72 (8): 1346–1367, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.jcss.2006.04.007">10.1016/j.jcss.2006.04.007</a></li>
<li><a href="/facts/Bruno_Courcelle/9148mMnR">Courcelle, Bruno</a> (1996), <a href="http://www.labri.fr/perso/courcell/Textes/DIMACS(1997).pdf">"On the expression of graph properties in some fragments of monadic second-order logic"</a> (PDF), in <a href="/facts/Neil_Immerman/7aCupltL">Immerman, Neil</a>; Kolaitis, Phokion G. (eds.), Proc. Descr. Complex. Finite Models, DIMACS, vol. 31, Amer. Math. Soc., pp. 33–62, <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.5184">10.1.1.55.5184</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1451381">1451381</a></li>
<li><a href="/facts/Bruno_Courcelle/9148mMnR">Courcelle, Bruno</a>; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138, <a href="/facts/Cambridge_University_Press/fgEBSSRq">Cambridge University Press</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9781139644006, <a href="/facts/Zbl_(identifier)/P6rFxKKx">Zbl</a> <a href="https://zbmath.org/?format=complete&q=an:1257.68006">1257.68006</a></li>
<li><a href="/facts/Bruno_Courcelle/9148mMnR">Courcelle, Bruno</a> (2018), "Fly-automata for checking MSO2 graph properties", <a href="/facts/Discrete_Applied_Mathematics/0xgV889h">Discrete Applied Mathematics</a>, 245: 236–252, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/1511.08605">1511.08605</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.dam.2016.10.018">10.1016/j.dam.2016.10.018</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3804787">3804787</a></li>
<li><a href="/facts/Bruno_Courcelle/9148mMnR">Courcelle, Bruno</a>; <a href="/facts/Oum_Sang-il/hTzPCJpv">Oum, Sang-il</a> (2007), <a href="http://mathsci.kaist.ac.kr/~sangil/pdf/2006co.pdf">"Vertex-minors, monadic second-order logic, and a conjecture by Seese"</a> (PDF), <a href="/facts/Journal_of_Combinatorial_Theory/oYS6G76K">Journal of Combinatorial Theory</a>, Series B, 97 (1): 91–126, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.jctb.2006.04.003">10.1016/j.jctb.2006.04.003</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2278126">2278126</a></li>
<li><a href="/facts/Rod_Downey/lVAAXpfF">Downey, R. G.</a>; <a href="/facts/Michael_Fellows/Mmlrxg5L">Fellows, M. R.</a> (1995), "Fixed-parameter tractability and completeness. II. On completeness for W[1]", <a href="/facts/Theoretical_Computer_Science_(journal)/Apbc0PDL">Theoretical Computer Science</a>, 141 (1–2): 109–131, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0304-3975%2894%2900097-3">10.1016/0304-3975(94)00097-3</a></li>
<li><a href="/facts/Zden%25C4%259Bk_Dvo%25C5%2599%25C3%25A1k/5JIfIyK0">Dvořák, Zdeněk</a>; <a href="/facts/Daniel_Kr%25C3%25A1%25C4%25BE/P6dcExDY">Kráľ, Daniel</a>; <a href="/facts/Robin_Thomas_(mathematician)/A3fS9arb">Thomas, Robin</a> (2010), "Deciding first-order properties for sparse graphs", <a href="/facts/Symposium_on_Foundations_of_Computer_Science/t0BvR59t">Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010)</a>, pp. 133–142, <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.170.9781">10.1.1.170.9781</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1109%2FFOCS.2010.20">10.1109/FOCS.2010.20</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-7695-4244-7, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3024787">3024787</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:15264036">15264036</a></li>
<li>Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995), Finite Model Theory, Springer Monographs in Mathematics (2nd ed.), Springer, p. 129, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F3-540-28788-4">10.1007/3-540-28788-4</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-540-28787-2</li>
<li>Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (October 2010), <a href="https://wwwmayr.in.tum.de/konferenzen/Sommerakademie2010/talks/tantau_paper.pdf">"Logspace Versions of the Theorems of Bodlaender and Courcelle"</a> (PDF), <a href="/facts/Symposium_on_Foundations_of_Computer_Science/t0BvR59t">Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010)</a>, pp. 143–152, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1109%2FFOCS.2010.21">10.1109/FOCS.2010.21</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4244-8525-3, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:1820251">1820251</a></li>
<li><a href="/facts/Ronald_Fagin/F8nzMq7b">Fagin, Ronald</a> (1976), <a href="https://scholar.archive.org/work/sfm46wwu45hqzmrfw2lrf6ztqa">"Probabilities on finite models"</a>, <a href="/facts/Journal_of_Symbolic_Logic/lfXVXcoy">Journal of Symbolic Logic</a>, 41 (1): 50–58, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1017%2Fs0022481200051756">10.1017/s0022481200051756</a>, <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2272945">2272945</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0476480">0476480</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:2563318">2563318</a></li>
<li><a href="/facts/Ronald_Fagin/F8nzMq7b">Fagin, Ronald</a>; <a href="/facts/Larry_Stockmeyer/9lx48AKu">Stockmeyer, Larry J.</a>; <a href="/facts/Moshe_Vardi/Sz9AoseQ">Vardi, Moshe Y.</a> (1995), "On monadic NP vs monadic co-NP", <a href="/facts/Information_and_Computation/4gdF7pR6">Information and Computation</a>, 120 (1): 78–92, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1006%2Finco.1995.1100">10.1006/inco.1995.1100</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1340807">1340807</a></li>
<li>Glebskiĭ, Ju. V.; Kogan, D. I.; Liogon'kiĭ, M. I.; Talanov, V. A. (1969), "Volume and fraction of satisfiability of formulas of the lower predicate calculus", Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika (2): 17–27, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0300882">0300882</a></li>
<li><a href="/facts/Leslie_Ann_Goldberg/0Qon5wnv">Goldberg, Leslie Ann</a> (1993), "Polynomial space polynomial delay algorithms for listing families of graphs", <a href="/facts/Symposium_on_Theory_of_Computing/xsemn7kG">Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing (STOC '93)</a>, New York, NY, USA: ACM, pp. 218–225, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F167088.167160">10.1145/167088.167160</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-89791-591-7, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:6305108">6305108</a></li>
<li>Grandjean, Étienne (1983), "Complexity of the first-order theory of almost all finite structures", <a href="/facts/Information_and_Computation/4gdF7pR6">Information and Control</a>, 57 (2–3): 180–204, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2FS0019-9958%2883%2980043-6">10.1016/S0019-9958(83)80043-6</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0742707">0742707</a></li>
<li><a href="/facts/Martin_Grohe/fVKhhhFq">Grohe, Martin</a> (2001), "Computing crossing numbers in quadratic time", <a href="/facts/Symposium_on_Theory_of_Computing/xsemn7kG">Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing (STOC '01)</a>, pp. 231–236, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/cs/0009010">cs/0009010</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F380752.380805">10.1145/380752.380805</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 1-58113-349-9, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:724544">724544</a></li>
<li><a href="/facts/Martin_Grohe/fVKhhhFq">Grohe, Martin</a> (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-107-01452-7, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479">3729479</a></li>
<li><a href="/facts/Martin_Grohe/fVKhhhFq">Grohe, Martin</a>; Kreutzer, Stephan; Siebertz, Sebastian (2014), "Deciding first-order properties of nowhere dense graphs", Proceedings of the 46th Annual ACM Symposium on Theory of Computing (STOC '14), New York: ACM, pp. 89–98, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/1311.3899">1311.3899</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F2591796.2591851">10.1145/2591796.2591851</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4503-2710-7, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:13297133">13297133</a></li>
<li>Hella, Lauri; Kolaitis, Phokion G.; Luosto, Kerkko (1996), "Almost everywhere equivalence of logics in finite model theory", The Bulletin of Symbolic Logic, 2 (4): 422–443, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F421173">10.2307/421173</a>, <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/421173">421173</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1460316">1460316</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:16411368">16411368</a></li>
<li>Henson, C. Ward (1972), "Countable homogeneous relational structures and 
 
 
 
 
 ℵ
 
 0
 
 
 
 
 {\displaystyle \aleph _{0}}
 
-categorical theories", The Journal of Symbolic Logic, 37: 494–500, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F2272734">10.2307/2272734</a>, <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/2272734">2272734</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0321727">0321727</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:40662635">40662635</a></li>
<li><a href="/facts/Neil_Immerman/7aCupltL">Immerman, Neil</a>; <a href="/facts/Eric_Lander/fDFnnbtM">Lander, Eric</a> (1990), "Describing graphs: a first-order approach to graph canonization", in <a href="/facts/Alan_Selman/PXolTPtl">Selman, Alan L.</a> (ed.), Complexity Theory Retrospective: In honor of Juris Hartmanis on the occasion of his sixtieth birthday, New York: Springer-Verlag, pp. 59–81, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-1-4612-4478-3_5">10.1007/978-1-4612-4478-3_5</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4612-8793-3, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1060782">1060782</a></li>
<li>Lavrov, I. A. (1963), "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., 2 (1): 5–18, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0157904">0157904</a></li>
<li><a href="/facts/Ken-ichi_Kawarabayashi/xKDg1l2u">Kawarabayashi, Ken-ichi</a>; <a href="/facts/Bruce_Reed_(mathematician)/rwrfNHpG">Reed, Bruce</a> (2007), "Computing crossing number in linear time", <a href="/facts/Symposium_on_Theory_of_Computing/xsemn7kG">Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC '07)</a>, pp. 382–390, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F1250790.1250848">10.1145/1250790.1250848</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-59593-631-8, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:13000831">13000831</a></li>
<li>Koncewicz, Leszek (1973), "Definability of classes of graphs in the first order predicate calculus with identity", Polish Academy of Sciences, 32: 159–190, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2FBF02123839">10.1007/BF02123839</a>, <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/20014678">20014678</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0351796">0351796</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:189786935">189786935</a></li>
<li>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, pp. 199–208, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/0911.3799">0911.3799</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1109%2FLICS.2010.42">10.1109/LICS.2010.42</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-4244-7588-9, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2963094">2963094</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:1450409">1450409</a></li>
<li>Libkin, Leonid (2004), <a href="https://archive.org/details/elementsoffinite00libk">Elements of finite model theory</a>, Texts in Theoretical Computer Science: An EATCS Series, Springer-Verlag, Berlin, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-3-662-07003-1">10.1007/978-3-662-07003-1</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 3-540-21202-7, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2102513">2102513</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:30176939">30176939</a></li>
<li>Lynch, James F. (1992), "Probabilities of sentences about very sparse random graphs", Random Structures & Algorithms, 3 (1): 33–53, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1002%2Frsa.3240030105">10.1002/rsa.3240030105</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1139487">1139487</a></li>
<li><a href="/facts/Jaroslav_Ne%25C5%25A1et%25C5%2599il/99pR0wFP">Nešetřil, Jaroslav</a>; <a href="/facts/Patrice_Ossona_de_Mendez/UdmKUVR7">Ossona de Mendez, Patrice</a> (2012), Sparsity: Graphs, Structures, and Algorithms, Algorithms and Combinatorics, vol. 28, Springer-Verlag, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-3-642-27875-4">10.1007/978-3-642-27875-4</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-642-27874-7, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2920058">2920058</a></li>
<li>Parys, Paweł (2014), "First-order logic on CPDA graphs", Computer science—theory and applications, <a href="/facts/Lecture_Notes_in_Computer_Science/1UeA77BC">Lecture Notes in Computer Science</a>, vol. 8476, New York: Springer-Verlag, pp. 300–313, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-3-319-06686-8_23">10.1007/978-3-319-06686-8_23</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-319-06685-1, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3218557">3218557</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:31640587">31640587</a></li>
<li>Pikhurko, Oleg; <a href="/facts/Joel_Spencer/dhg8jEo4">Spencer, Joel</a>; Verbitsky, Oleg (2006), "Succinct definitions in the first order theory of graphs", Annals of Pure and Applied Logic, 139 (1–3): 74–109, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/math/0401307">math/0401307</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.apal.2005.04.003">10.1016/j.apal.2005.04.003</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2206252">2206252</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:3041191">3041191</a></li>
<li>Pikhurko, Oleg; Verbitsky, Oleg (2011), <a href="https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129">"Logical complexity of graphs: a survey"</a>, in <a href="/facts/Martin_Grohe/fVKhhhFq">Grohe, Martin</a>; Makowsky, Johann A. (eds.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, January 5-8, 2009, Washington, DC), Contemporary Mathematics, vol. 558, American Mathematical Society, pp. 129–180, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/1003.4865">1003.4865</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-8218-8322-8</li>
<li>Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic, 53 (2): 169–195, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0168-0072%2891%2990054-P">10.1016/0168-0072(91)90054-P</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1114848">1114848</a></li>
<li><a href="/facts/Saharon_Shelah/oI5WSK8p">Shelah, Saharon</a>; <a href="/facts/Joel_Spencer/dhg8jEo4">Spencer, Joel</a> (1988), "Zero-one laws for sparse random graphs", <a href="/facts/Journal_of_the_American_Mathematical_Society/qR98drCm">Journal of the American Mathematical Society</a>, 1 (1): 97–115, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F1990968">10.2307/1990968</a>, <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/1990968">1990968</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0924703">0924703</a></li>
<li><a href="/facts/Joel_Spencer/dhg8jEo4">Spencer, Joel</a> (1990), "Infinite spectra in the first order theory of graphs", <a href="/facts/Combinatorica/AxdqUqrp">Combinatorica</a>, 10 (1): 95–102, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2FBF02122699">10.1007/BF02122699</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1075070">1075070</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:27770505">27770505</a></li>
<li><a href="/facts/Joel_Spencer/dhg8jEo4">Spencer, Joel</a> (2001), <a href="/facts/The_Strange_Logic_of_Random_Graphs/f44hfBSP">The Strange Logic of Random Graphs</a>, Algorithms and Combinatorics, vol. 22, Springer-Verlag, Berlin, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1007%2F978-3-662-04538-1">10.1007/978-3-662-04538-1</a>, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 3-540-41654-4, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1847951">1847951</a></li>
<li><a href="/facts/Boris_Trakhtenbrot/oftNXKRM">Trahtenbrot, B. A.</a> (1950), "The impossibility of an algorithm for the decision problem for finite domains", Doklady Akademii Nauk SSSR, New Series, 70: 569–572, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0033784">0033784</a></li>
<li>Verbitsky, Oleg (2005), "The first order definability of graphs with separators via the Ehrenfeucht game", <a href="/facts/Theoretical_Computer_Science_(journal)/Apbc0PDL">Theoretical Computer Science</a>, 343 (1–2): 158–176, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/math/0401361">math/0401361</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.tcs.2005.05.003">10.1016/j.tcs.2005.05.003</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=2168849">2168849</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:17886484">17886484</a></li>
<li>Verbitsky, Oleg; Zhukovskii, Maksim (2019), "Tight bounds on the asymptotic descriptive complexity of subgraph isomorphism", ACM Transactions on Computational Logic, 20 (2): A9:1–A9:18, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/1802.02143">1802.02143</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1145%2F3303881">10.1145/3303881</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3942556">3942556</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:3603039">3603039</a></li>
<li>Zeume, Thomas (2017), <a href="https://informatik-rub.de/wp-content/uploads/2021/03/Zeume2017-dynclique-journal.pdf">"The dynamic descriptive complexity of k-clique"</a> (PDF), <a href="/facts/Information_and_Computation/4gdF7pR6">Information and Computation</a>, 256: 9–22, <a href="/facts/ArXiv_(identifier)/H6EtgnBe">arXiv</a>:<a href="https://arxiv.org/abs/1610.09089">1610.09089</a>, <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fj.ic.2017.04.005">10.1016/j.ic.2017.04.005</a>, <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3705411">3705411</a>, <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:1412001">1412001</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Spencer (2001), Section 1.2, "What Is a First Order Theory?", pp. 15–17. - Spencer, Joel (2001), The Strange Logic of Random Graphs, Algorithms and Combinatorics, vol. 22, Springer-Verlag, Berlin, doi:10.1007/978-3-662-04538-1, ISBN 3-540-41654-4, MR 1847951 <a href="https://doi.org/10.1007%2F978-3-662-04538-1" target="_blank">https://doi.org/10.1007%2F978-3-662-04538-1</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Spencer (2001), Section 1.2, "What Is a First Order Theory?", pp. 15–17. - Spencer, Joel (2001), The Strange Logic of Random Graphs, Algorithms and Combinatorics, vol. 22, Springer-Verlag, Berlin, doi:10.1007/978-3-662-04538-1, ISBN 3-540-41654-4, MR 1847951 <a href="https://doi.org/10.1007%2F978-3-662-04538-1" target="_blank">https://doi.org/10.1007%2F978-3-662-04538-1</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Verbitsky & Zhukovskii (2019). - Verbitsky, Oleg; Zhukovskii, Maksim (2019), "Tight bounds on the asymptotic descriptive complexity of subgraph isomorphism", ACM Transactions on Computational Logic, 20 (2): A9:1–A9:18, arXiv:1802.02143, doi:10.1145/3303881, MR 3942556, S2CID 3603039 <a href="https://arxiv.org/abs/1802.02143" target="_blank">https://arxiv.org/abs/1802.02143</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Zeume (2017). - Zeume, Thomas (2017), "The dynamic descriptive complexity of k-clique" (PDF), Information and Computation, 256: 9–22, arXiv:1610.09089, doi:10.1016/j.ic.2017.04.005, MR 3705411, S2CID 1412001 <a href="https://informatik-rub.de/wp-content/uploads/2021/03/Zeume2017-dynclique-journal.pdf" target="_blank">https://informatik-rub.de/wp-content/uploads/2021/03/Zeume2017-dynclique-journal.pdf</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">Goldberg (1993). - Goldberg, Leslie Ann (1993), "Polynomial space polynomial delay algorithms for listing families of graphs", Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing (STOC '93), New York, NY, USA: ACM, pp. 218–225, doi:10.1145/167088.167160, ISBN 0-89791-591-7, S2CID 6305108 <a href="https://doi.org/10.1145%2F167088.167160" target="_blank">https://doi.org/10.1145%2F167088.167160</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">For instance, Henson (1972) requires directed graphs to be described by an asymmetric relation, meaning that loops and 2-cycles are both disallowed, giving the oriented graphs. - Henson, C. Ward (1972), "Countable homogeneous relational structures and 
 
 
 
 
 ℵ
 
 0
 
 
 
 
 {\displaystyle \aleph _{0}}
 
-categorical theories", The Journal of Symbolic Logic, 37: 494–500, doi:10.2307/2272734, JSTOR 2272734, MR 0321727, S2CID 40662635 <a href="https://doi.org/10.2307%2F2272734" target="_blank">https://doi.org/10.2307%2F2272734</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Koncewicz (1973). - Koncewicz, Leszek (1973), "Definability of classes of graphs in the first order predicate calculus with identity", Polish Academy of Sciences, 32: 159–190, doi:10.1007/BF02123839, JSTOR 20014678, MR 0351796, S2CID 189786935 <a href="https://doi.org/10.1007%2FBF02123839" target="_blank">https://doi.org/10.1007%2FBF02123839</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Bruggink & König (2018). - Bruggink, H. J. Sander; König, Barbara (2018), "Recognizable languages of arrows and cospans", Mathematical Structures in Computer Science, 28 (8): 1290–1332, doi:10.1017/S096012951800018X, MR 3849613, S2CID 52275704 <a href="https://doi.org/10.1017%2FS096012951800018X" target="_blank">https://doi.org/10.1017%2FS096012951800018X</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Glebskiĭ et al. (1969); Fagin (1976) - Glebskiĭ, Ju. V.; Kogan, D. I.; Liogon'kiĭ, M. I.; Talanov, V. A. (1969), "Volume and fraction of satisfiability of formulas of the lower predicate calculus", Otdelenie Matematiki, Mekhaniki i Kibernetiki Akademii Nauk Ukrainskoĭ SSR: Kibernetika (2): 17–27, MR 0300882 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0300882" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=0300882</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Grandjean (1983). - Grandjean, Étienne (1983), "Complexity of the first-order theory of almost all finite structures", Information and Control, 57 (2–3): 180–204, doi:10.1016/S0019-9958(83)80043-6, MR 0742707 <a href="https://doi.org/10.1016%2FS0019-9958%2883%2980043-6" target="_blank">https://doi.org/10.1016%2FS0019-9958%2883%2980043-6</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Goldberg (1993). - Goldberg, Leslie Ann (1993), "Polynomial space polynomial delay algorithms for listing families of graphs", Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing (STOC '93), New York, NY, USA: ACM, pp. 218–225, doi:10.1145/167088.167160, ISBN 0-89791-591-7, S2CID 6305108 <a href="https://doi.org/10.1145%2F167088.167160" target="_blank">https://doi.org/10.1145%2F167088.167160</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">Shelah & Spencer (1988); Spencer (2001). - Shelah, Saharon; Spencer, Joel (1988), "Zero-one laws for sparse random graphs", Journal of the American Mathematical Society, 1 (1): 97–115, doi:10.2307/1990968, JSTOR 1990968, MR 0924703 <a href="https://doi.org/10.2307%2F1990968" target="_blank">https://doi.org/10.2307%2F1990968</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
<li id="fn:13">Lynch (1992). - Lynch, James F. (1992), "Probabilities of sentences about very sparse random graphs", Random Structures & Algorithms, 3 (1): 33–53, doi:10.1002/rsa.3240030105, MR 1139487 <a href="https://doi.org/10.1002%2Frsa.3240030105" target="_blank">https://doi.org/10.1002%2Frsa.3240030105</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></li>
<li id="fn:14">Spencer (1990). - Spencer, Joel (1990), "Infinite spectra in the first order theory of graphs", Combinatorica, 10 (1): 95–102, doi:10.1007/BF02122699, MR 1075070, S2CID 27770505 <a href="https://doi.org/10.1007%2FBF02122699" target="_blank">https://doi.org/10.1007%2FBF02122699</a> <a href="#fnref:14" class="footnote-back-ref">↩</a></li>
<li id="fn:15">Downey & Fellows (1995). - Downey, R. G.; Fellows, M. R. (1995), "Fixed-parameter tractability and completeness. II. On completeness for W[1]", Theoretical Computer Science, 141 (1–2): 109–131, doi:10.1016/0304-3975(94)00097-3 <a href="https://doi.org/10.1016%2F0304-3975%2894%2900097-3" target="_blank">https://doi.org/10.1016%2F0304-3975%2894%2900097-3</a> <a href="#fnref:15" class="footnote-back-ref">↩</a></li>
<li id="fn:16">Chen et al. (2006). - Chen, Jianer; Huang, Xiuzhen; Kanj, Iyad A.; Xia, Ge (2006), "Strong computational lower bounds via parameterized complexity", Journal of Computer and System Sciences, 72 (8): 1346–1367, doi:10.1016/j.jcss.2006.04.007 <a href="https://doi.org/10.1016%2Fj.jcss.2006.04.007" target="_blank">https://doi.org/10.1016%2Fj.jcss.2006.04.007</a> <a href="#fnref:16" class="footnote-back-ref">↩</a></li>
<li id="fn:17">Nešetřil & Ossona de Mendez (2012), 18.3 The Subgraph Isomorphism Problem and Boolean Queries, pp. 400–401; Dvořák, Kráľ & Thomas (2010); Grohe, Kreutzer & Siebertz (2014). - Nešetřil, Jaroslav; Ossona de Mendez, Patrice (2012), Sparsity: Graphs, Structures, and Algorithms, Algorithms and Combinatorics, vol. 28, Springer-Verlag, doi:10.1007/978-3-642-27875-4, ISBN 978-3-642-27874-7, MR 2920058 <a href="https://doi.org/10.1007%2F978-3-642-27875-4" target="_blank">https://doi.org/10.1007%2F978-3-642-27875-4</a> <a href="#fnref:17" class="footnote-back-ref">↩</a></li>
<li id="fn:18">Pikhurko, Spencer & Verbitsky (2006). - Pikhurko, Oleg; Spencer, Joel; Verbitsky, Oleg (2006), "Succinct definitions in the first order theory of graphs", Annals of Pure and Applied Logic, 139 (1–3): 74–109, arXiv:math/0401307, doi:10.1016/j.apal.2005.04.003, MR 2206252, S2CID 3041191 <a href="https://arxiv.org/abs/math/0401307" target="_blank">https://arxiv.org/abs/math/0401307</a> <a href="#fnref:18" class="footnote-back-ref">↩</a></li>
<li id="fn:19">Pikhurko & Verbitsky (2011). - Pikhurko, Oleg; Verbitsky, Oleg (2011), "Logical complexity of graphs: a survey", in Grohe, Martin; Makowsky, Johann A. (eds.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, January 5-8, 2009, Washington, DC), Contemporary Mathematics, vol. 558, American Mathematical Society, pp. 129–180, arXiv:1003.4865, ISBN 978-0-8218-8322-8 <a href="https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129" target="_blank">https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129</a> <a href="#fnref:19" class="footnote-back-ref">↩</a></li>
<li id="fn:20">Pikhurko & Verbitsky (2011). - Pikhurko, Oleg; Verbitsky, Oleg (2011), "Logical complexity of graphs: a survey", in Grohe, Martin; Makowsky, Johann A. (eds.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, January 5-8, 2009, Washington, DC), Contemporary Mathematics, vol. 558, American Mathematical Society, pp. 129–180, arXiv:1003.4865, ISBN 978-0-8218-8322-8 <a href="https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129" target="_blank">https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129</a> <a href="#fnref:20" class="footnote-back-ref">↩</a></li>
<li id="fn:21">Verbitsky (2005). - Verbitsky, Oleg (2005), "The first order definability of graphs with separators via the Ehrenfeucht game", Theoretical Computer Science, 343 (1–2): 158–176, arXiv:math/0401361, doi:10.1016/j.tcs.2005.05.003, MR 2168849, S2CID 17886484 <a href="https://arxiv.org/abs/math/0401361" target="_blank">https://arxiv.org/abs/math/0401361</a> <a href="#fnref:21" class="footnote-back-ref">↩</a></li>
<li id="fn:22">Pikhurko & Verbitsky (2011). - Pikhurko, Oleg; Verbitsky, Oleg (2011), "Logical complexity of graphs: a survey", in Grohe, Martin; Makowsky, Johann A. (eds.), Model Theoretic Methods in Finite Combinatorics (AMS-ASL Joint Special Session, January 5-8, 2009, Washington, DC), Contemporary Mathematics, vol. 558, American Mathematical Society, pp. 129–180, arXiv:1003.4865, ISBN 978-0-8218-8322-8 <a href="https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129" target="_blank">https://books.google.com/books?id=5kfVAwAAQBAJ&pg=PA129</a> <a href="#fnref:22" class="footnote-back-ref">↩</a></li>
<li id="fn:23">Immerman & Lander (1990). - Immerman, Neil; Lander, Eric (1990), "Describing graphs: a first-order approach to graph canonization", in Selman, Alan L. (ed.), Complexity Theory Retrospective: In honor of Juris Hartmanis on the occasion of his sixtieth birthday, New York: Springer-Verlag, pp. 59–81, doi:10.1007/978-1-4612-4478-3_5, ISBN 978-1-4612-8793-3, MR 1060782 <a href="https://doi.org/10.1007%2F978-1-4612-4478-3_5" target="_blank">https://doi.org/10.1007%2F978-1-4612-4478-3_5</a> <a href="#fnref:23" class="footnote-back-ref">↩</a></li>
<li id="fn:24">Ebbinghaus & Flum (1995). Parys (2014) writes that this undecidability result is well known, and attributes it to Trahtenbrot (1950) on the undecidability of first-order satisfiability for more general classes of finite structures. - Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995), Finite Model Theory, Springer Monographs in Mathematics (2nd ed.), Springer, p. 129, doi:10.1007/3-540-28788-4, ISBN 978-3-540-28787-2 <a href="https://doi.org/10.1007%2F3-540-28788-4" target="_blank">https://doi.org/10.1007%2F3-540-28788-4</a> <a href="#fnref:24" class="footnote-back-ref">↩</a></li>
<li id="fn:25">Lavrov (1963). - Lavrov, I. A. (1963), "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., 2 (1): 5–18, MR 0157904 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0157904" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=0157904</a> <a href="#fnref:25" class="footnote-back-ref">↩</a></li>
<li id="fn:26">Grohe (2017), pp. 23–27. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:26" class="footnote-back-ref">↩</a></li>
<li id="fn:27">Grohe (2017), pp. 23–27. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:27" class="footnote-back-ref">↩</a></li>
<li id="fn:28">Grohe (2017), pp. 23–27. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:28" class="footnote-back-ref">↩</a></li>
<li id="fn:29">Grohe (2017), pp. 50–51. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:29" class="footnote-back-ref">↩</a></li>
<li id="fn:30">Cai, Fürer & Immerman (1992). - Cai, Jin-Yi; Fürer, Martin; Immerman, Neil (1992), "An optimal lower bound on the number of variables for graph identification", Combinatorica, 12 (4): 389–410, doi:10.1007/BF01305232, MR 1194730 <a href="https://doi.org/10.1007%2FBF01305232" target="_blank">https://doi.org/10.1007%2FBF01305232</a> <a href="#fnref:30" class="footnote-back-ref">↩</a></li>
<li id="fn:31">Grohe (2017), pp. 50–51. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:31" class="footnote-back-ref">↩</a></li>
<li id="fn:32">Hella, Kolaitis & Luosto (1996). - Hella, Lauri; Kolaitis, Phokion G.; Luosto, Kerkko (1996), "Almost everywhere equivalence of logics in finite model theory", The Bulletin of Symbolic Logic, 2 (4): 422–443, doi:10.2307/421173, JSTOR 421173, MR 1460316, S2CID 16411368 <a href="https://doi.org/10.2307%2F421173" target="_blank">https://doi.org/10.2307%2F421173</a> <a href="#fnref:32" class="footnote-back-ref">↩</a></li>
<li id="fn:33">Grohe (2017), pp. 50–51. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:33" class="footnote-back-ref">↩</a></li>
<li id="fn:34">Laubner (2010). - 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, pp. 199–208, arXiv:0911.3799, doi:10.1109/LICS.2010.42, ISBN 978-1-4244-7588-9, MR 2963094, S2CID 1450409 <a href="https://arxiv.org/abs/0911.3799" target="_blank">https://arxiv.org/abs/0911.3799</a> <a href="#fnref:34" class="footnote-back-ref">↩</a></li>
<li id="fn:35">Grohe (2017), pp. 50–51. - Grohe, Martin (2017), Descriptive complexity, canonisation, and definable graph structure theory, Lecture Notes in Logic, vol. 47, Cambridge University Press, Cambridge, ISBN 978-1-107-01452-7, MR 3729479 <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=3729479" target="_blank">https://mathscinet.ams.org/mathscinet-getitem?mr=3729479</a> <a href="#fnref:35" class="footnote-back-ref">↩</a></li>
<li id="fn:36">These definitions can be found e.g. in Courcelle & Engelfriet (2012), p. 69, under the slightly different notation MS1 and MS2. Other authors used the MSO1 and MSO2 notations, and Courcelle came to use it later as well; see, e.g., Courcelle (2018). - Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006 <a href="https://zbmath.org/?format=complete&q=an:1257.68006" target="_blank">https://zbmath.org/?format=complete&q=an:1257.68006</a> <a href="#fnref:36" class="footnote-back-ref">↩</a></li>
<li id="fn:37">Fagin, Stockmeyer & Vardi (1995). - 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 <a href="https://doi.org/10.1006%2Finco.1995.1100" target="_blank">https://doi.org/10.1006%2Finco.1995.1100</a> <a href="#fnref:37" class="footnote-back-ref">↩</a></li>
<li id="fn:38">Courcelle & Engelfriet (2012); Libkin (2004), Corollary 7.24, pp. 126–127. - Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006 <a href="https://zbmath.org/?format=complete&q=an:1257.68006" target="_blank">https://zbmath.org/?format=complete&q=an:1257.68006</a> <a href="#fnref:38" class="footnote-back-ref">↩</a></li>
<li id="fn:39">Courcelle (1996). - Courcelle, Bruno (1996), "On the expression of graph properties in some fragments of monadic second-order logic" (PDF), in Immerman, Neil; Kolaitis, Phokion G. (eds.), Proc. Descr. Complex. Finite Models, DIMACS, vol. 31, Amer. Math. Soc., pp. 33–62, CiteSeerX 10.1.1.55.5184, MR 1451381 <a href="http://www.labri.fr/perso/courcell/Textes/DIMACS(1997).pdf" target="_blank">http://www.labri.fr/perso/courcell/Textes/DIMACS(1997).pdf</a> <a href="#fnref:39" class="footnote-back-ref">↩</a></li>
<li id="fn:40">Courcelle & Engelfriet (2012). - Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006 <a href="https://zbmath.org/?format=complete&q=an:1257.68006" target="_blank">https://zbmath.org/?format=complete&q=an:1257.68006</a> <a href="#fnref:40" class="footnote-back-ref">↩</a></li>
<li id="fn:41">Elberfeld, Jakoby & Tantau (2010). - Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (October 2010), "Logspace Versions of the Theorems of Bodlaender and Courcelle" (PDF), Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), pp. 143–152, doi:10.1109/FOCS.2010.21, ISBN 978-1-4244-8525-3, S2CID 1820251 <a href="https://wwwmayr.in.tum.de/konferenzen/Sommerakademie2010/talks/tantau_paper.pdf" target="_blank">https://wwwmayr.in.tum.de/konferenzen/Sommerakademie2010/talks/tantau_paper.pdf</a> <a href="#fnref:41" class="footnote-back-ref">↩</a></li>
<li id="fn:42">Grohe (2001); Kawarabayashi & Reed (2007). - Grohe, Martin (2001), "Computing crossing numbers in quadratic time", Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing (STOC '01), pp. 231–236, arXiv:cs/0009010, doi:10.1145/380752.380805, ISBN 1-58113-349-9, S2CID 724544 <a href="https://arxiv.org/abs/cs/0009010" target="_blank">https://arxiv.org/abs/cs/0009010</a> <a href="#fnref:42" class="footnote-back-ref">↩</a></li>
<li id="fn:43">Courcelle & Oum (2007). - Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-minors, monadic second-order logic, and a conjecture by Seese" (PDF), Journal of Combinatorial Theory, Series B, 97 (1): 91–126, doi:10.1016/j.jctb.2006.04.003, MR 2278126 <a href="http://mathsci.kaist.ac.kr/~sangil/pdf/2006co.pdf" target="_blank">http://mathsci.kaist.ac.kr/~sangil/pdf/2006co.pdf</a> <a href="#fnref:43" class="footnote-back-ref">↩</a></li>
<li id="fn:44">Seese (1991). - Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic, 53 (2): 169–195, doi:10.1016/0168-0072(91)90054-P, MR 1114848 <a href="https://doi.org/10.1016%2F0168-0072%2891%2990054-P" target="_blank">https://doi.org/10.1016%2F0168-0072%2891%2990054-P</a> <a href="#fnref:44" class="footnote-back-ref">↩</a></li>
<li id="fn:45">Courcelle & Oum (2007). - Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-minors, monadic second-order logic, and a conjecture by Seese" (PDF), Journal of Combinatorial Theory, Series B, 97 (1): 91–126, doi:10.1016/j.jctb.2006.04.003, MR 2278126 <a href="http://mathsci.kaist.ac.kr/~sangil/pdf/2006co.pdf" target="_blank">http://mathsci.kaist.ac.kr/~sangil/pdf/2006co.pdf</a> <a href="#fnref:45" class="footnote-back-ref">↩</a></li>
</ol>

Logic of graphs open-in-new

Logic of graphs