An Optimal Construction for the Barthelmann-Schwentick Normal Form on Classes of Structures of Bounded Degree.

Building on the locality conditions for first-order logic by Hanf and Gaifman, Barthelmann and Schwentick showed in 1999 that every first-order formula is equivalent to a formula of the shape $exists x_1 dotsc exists x_k forall y,phi$ where quantification in $phi$ is relativised to elements of distance $leq r$ from $y$. Such a formula will be called Barthelmann-Schwentick normal form (BSNF) in the following. However, although the proof is effective, it leads to a non-elementary blow-up of the BSNF in terms of the size of the original formula. show that, if equivalence on the class of all structures, or even only finite forests, is required, this non-elementary blow-up is indeed unavoidable. We then examine restricted classes of structures where more efficient algorithms are possible. In this direction, we show that on any class of structures of degree $leq 2$, BSNF can be computed in 2-fold exponential time with respect to the size of the input formula. And for any class of structures of degree $leq d$ for some $dgeq 3$, this is possible in 3-fold exponential time. For both cases, we provide matching lower bounds.