Here is a collection of logical formulas demonstrating the computational complexity of certain problems. Note that the quoted complexity class corrsponds to the formula, not the actual known complexity class.

(c.f. Existential Second-Order Logic Over Graphs: A Complete Complexity-Theoretic Classification for the syntax-complexity correspondances)

Decision problems for basic graphs, in which E represents the edge relation, unary relations are represented as Cx for C(x), and binary relations R are represented as xRy for R(x,y). Below the table are some formulas expressing some first order properties and the notation used:

Problem | Class | Formula | Quantifier form |
---|---|---|---|

2-Colourable | L | ∃C ∀uv (uEv → ¬((Cu∧Cv)∨(¬Cu∧¬Cv))) | Eaa |

Disconnected | NL | ∃E ∃xy∀uv (Cx∧¬Cy)∧((Cu∧¬Cv) → ¬uEv) | E_{1}e*aa |

Square Root | NP | ∃R ∀uv R⊆E∧(uEv ↔ (uRv∨uR²v)) | Eaaae |

not-CIS | NP | ∃CS (MAXCLIQUE(C)∧MAXSTABLE(S)∧∀u¬(Cu∧Su)) | E*(ae)* |

Property | Formula | Notation |
---|---|---|

All edges of R are edges of E | ∀uv (uRv → uEv) | R⊆E |

There is a vertex between u and v for the relation R | ∃w(uRw∧wRv) | uR²v |

C is a maximal clique | ∀uv((Cu∧Cv∧u≠v) → uEv)∧∀u(¬Cu → ∃v(Cv∧¬uEv)) | MAXCLIQUE(C) |

C is a maximal stable set | ∀uv((Cu∧Cv) → ¬uEv)∧∀u(¬Cu → ∃v(Cv∧uEv)) | MAXSTABLE(C) |

Decision problems for knots, with an untwisted link diagram represented as a directed graph G with vertices V, edges E, functions s, e from V to E signifying the start and end vertices of an edge, and a binary relation O(v,e) signifying that the crossing at he vertex v of the edge e at the vertex is "over". When not explicit, large AND symbols are over all the non-specified parameters.

Problem | Class | Formula | Quantifier form |
---|---|---|---|

Tricolourability | NP | ∃C_{1}C_{2}C_{3}(⋀∃uC_{i}u)∧∀u(⋀_{i≠j}¬C_{i}u∧C_{j}u)∧∀uefgh(V(u,e,f,g,h) →
(⋀(C_{i}e ↔ C_{i}f)∧(⋀_{k=g,h}¬(C_{i}e∧C_{i}k))∧(⋀¬C_{i}g∧C_{i}h))) |
E*(ae)* |

Property | Formula | Notation |
---|---|---|

v is a vertex with edges e,f,g,h, with e and g ending at v, f and h starting at v, and e,f correspond to the arc passing over the crossing | s(e)=v∧s(g)=v∧t(f)=v∧t(h)=v∧O(v,e)∧O(v,f)∧¬O(v,g)∧¬O(v,h) | V(v,e,f,g,h) |