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片段的可满足性问题是可判定的。另一方面，扩大半径会导致不可判定性。在第二部分，我们精确描绘了局部逻辑存在片段的可满足性问题的判定性与复杂性图景，这些片段由每个元素携带的数据值数量以及所考虑邻域的半径参数化。总而言之，我们描绘了适用于带数据系统规约的形式化方法图景，并为未来研究开辟了新途径。