发表机构
Humboldt-Universität zu Berlin; RWTH Aachen University(柏林洪堡大学; 亚琛工业大学)
机构由 AI 辅助整理,请以论文原文为准。AI 中文总结
本文提出保秩Gaifman范式定理,适用于一阶逻辑及带模计数量词和加权结构逻辑ngFOW+,简化了无处稠密结构上近线性时间算法的元定理证明。
AI 中文摘要
我们证明了Gaifman定理的一个保秩版本。与早期保秩局部性定理(特别是[Grohe, Kreutzer, Siebertz, JACM 2017])相比,我们的定理更简单,并生成与Gaifman原始定理完全相同的范式公式。此外,它不仅适用于一阶逻辑,还适用于带模计数量词的一阶逻辑,更一般地,适用于本文引入的加权结构上的一阶逻辑ngFOW+。作为我们定理的一个应用,我们给出了[Grohe, Kreutzer, Siebertz, JACM 2017]算法元定理的简化证明,该定理指出无处稠密结构的一阶性质可以在近线性时间内判定。我们针对权重逻辑ngFOW+的局部性定理可被视为迈向该逻辑的此类元定理的关键一步。
英文摘要
We prove a rank-preserving version of Gaifman's Theorem. Compared to earlier rank-preserving locality theorems (in particular, [Grohe, Kreutzer, Siebertz, JACM 2017]), our theorem is much simpler and yields formulas in exactly the same normal form as Gaifman's original theorem. Furthermore, it holds not only for first-order logic, but also for first-order logic with modulo-counting quantifiers and, more generally, for the first-order logic on weighted structures ngFOW+ that is introduced in this article. As an application of our theorem, we give a simplified proof of the algorithmic meta-theorem of [Grohe, Kreutzer, Siebertz, JACM 2017] stating that first-order properties of nowhere dense structures can be decided in almost-linear time. Our locality theorem for the weight logic ngFOW+ can be seen as an essential step toward such a meta-theorem for this logic.
Comments54 pages, 1 figure. This paper supersedes the preprint arXiv:2606.11993