  In general, a graph modification problem is defined by a graph modification
operation $\boxtimes$ and a target graph property ${\cal P}$. Typically, the
modification operation $\boxtimes$ may be vertex removal}, edge removal}, edge
contraction}, or edge addition and the question is, given a graph $G$ and an
integer $k$, whether it is possible to transform $G$ to a graph in ${\cal P}$
after applying $k$ times the operation $\boxtimes$ on $G$. This problem has
been extensively studied for particilar instantiations of $\boxtimes$ and
${\cal P}$. In this paper we consider the general property ${\cal P}_{{\phi}}$
of being planar and, moreover, being a model of some First-Order Logic sentence
${\phi}$ (an FOL-sentence). We call the corresponding meta-problem Graph
$\boxtimes$-Modification to Planarity and ${\phi}$ and prove the following
algorithmic meta-theorem: there exists a function $f:\Bbb{N}^{2}\to\Bbb{N}$
such that, for every $\boxtimes$ and every FOL sentence ${\phi}$, the Graph
$\boxtimes$-Modification to Planarity and ${\phi}$ is solvable in
$f(k,|{\phi}|)\cdot n^2$ time. The proof constitutes a hybrid of two different
classic techniques in graph algorithms. The first is the irrelevant vertex
technique that is typically used in the context of Graph Minors and deals with
properties such as planarity or surface-embeddability (that are not
FOL-expressible) and the second is the use of Gaifman's Locality Theorem that
is the theoretical base for the meta-algorithmic study of FOL-expressible
problems.
