The monadic second-order logic of graphs. XII: Planar graphs and planar maps (Q1566702)

[For the previous paper in this series see Zbl 0938.03015.] As shown in several previous papers by the author, many important graph properties and constructions can be expressed in monadic second-order (MSO) logic. Here the MSO definability of planar embeddings of certain kinds of graphs is considered. A planar embedding of a graph is a relational structure that describes a circular ordering of the neighbourhood of each vertex. A graph is 3-connected if it has at least four vertices, is 2-connected and has no separating pair. It is shown that the planar embedding (unique by a theorem due to Whitney) of a 3-connected planar graph is MSO definable. Also for planar graphs which are not 3-connected, a planar embedding can be specified assuming that a linear order of the edges is given, but it is also shown that the ordering is really needed. Many of the constructions can be expressed by a new extension of first-order logic which includes special atomic formulae for representing the transitive closures of binary relations.