A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures

arXiv (Cornell University)

Abstract

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.

Authors 4

1. Steffen van Bergerem

   Humboldt-Universität zu Berlin

   Affiliation as printed

   Humboldt-Universität zu Berlin , Germany

2. Martin Grohe Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

3. Charlotte Lenz Aachen

   RWTH Aachen University · Humboldt-Universität zu Berlin

   Affiliation as printed

   Humboldt-Universität zu Berlin , Germany

   RWTH Aachen University , Germany

4. Nicole Schweikardt

   Humboldt-Universität zu Berlin

   Affiliation as printed

   Humboldt-Universität zu Berlin , Germany