We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we introduce a family of local fragments. They restrict quantification to the neighbourhood of a given reference point that is bounded by some radius. Our first main result establishes decidability of the satisfiability problem for the local radius-1 fragment in presence of one ``diagonal relation''. On the other hand, extending the radius leads to undecidability. In a second part, we provide the precise decidability and complexity landscape of the satisfiability problem for the existential fragments of local logic, which are parameterized by the number of data values carried by each element and the radius of the considered neighbourhoods. Altogether, we draw a landscape of formalisms that are suitable for the specification of systems with data and open up new avenues for future research.

翻译：本文研究无序结构上的一阶逻辑，其中元素携带来自无穷域的有限个数据值，这些数据值可进行相等性比较。由于该逻辑的可满足性问题一般情况下不可判定，我们引入了一族局部片段，将量词限定在由给定参考点出发、半径有界的邻域内。首个主要结果表明：在存在一个"对角关系"的情况下，局部半径-1片段的可满足性问题可判定；而拓展半径则会导致不可判定性。在第二部分中，我们完整刻画了局部逻辑存在性片段可满足性问题的可判定性与复杂度全景图，这些片段以每个元素携带的数据值数量和所考虑邻域的半径为参数。综上，我们勾勒出了一套适用于描述带数据系统的形式体系，并为未来研究开辟了新方向。