有界度结构类上Barthelmann-Schwentick范式的优化构造

基于 Hanf 与 Gaifman 的一阶逻辑局部性条件，Barthelmann 与 Schwentick 于 1999 年证明每个一阶公式都等价于形如 $\exists x_1 \dotsc \exists x_k \forall y\,\phi$ 的公式，其中 $\phi$ 中的量化被限制为距 $y$ 距离 $\leq r$ 的元素。下文将此类公式称为 Barthelmann-Schwentick 范式（BSNF）。然而，尽管该证明是有效的，它导致 BSNF 相对于原公式规模呈非初等膨胀。我们证明，若要求在所有结构类甚至仅有限森林上等价，此非初等膨胀确实不可避免。随后我们考察可进行更高效算法的受限结构类。就此，我们证明在度 $\leq 2$ 的任意结构类上，BSNF 可相对于输入公式规模在二重指数时间内算出；而对度 $\leq d$（$d\geq 3$）的任意结构类，则可在三重指数时间内实现。对两种情况我们都给出了匹配的下界。