A Rank-Preserving Locality Theorem
2026-06-22 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors proved a new version of a theorem that deals with how certain logic formulas can be broken down based on graph structure, keeping the same complexity level. This theorem is similar to previous work on logic locality but allows a simpler type of sentence called weak scatter sentences, which can be checked faster. Their improvement is important when working with graphs that have a specific property called bounded merge-width. Essentially, the authors made it easier and more efficient to analyze logical properties on these graphs.
Gaifman's locality theoremfirst-order logicrank-preserving localityscatter sentencesgraph theorybounded merge-widthsyntactic variantlogical localityalgorithmic graph theory
Authors
Jan Dreier, Szymon Toruńczyk
Abstract
We prove a rank-preserving locality theorem for a syntactic variant of first-order logic, in the spirit of Gaifman's locality theorem and the rank-preserving locality theorem of Grohe, Kreutzer, and Siebertz. Our result allows for a weak form of scatter sentences, which can be evaluated more efficiently than usual scatter sentences considered in prior work. This is crucial in our application to graphs of bounded merge-width.