一句话：研究带数据局部一阶逻辑片段的可满足性，给出半径1片段可判定及存在片段复杂度全景。
本文研究无序结构上带数据值的一阶逻辑：每个元素携带有限个来自无限域的数据，数据间仅可比较相等。由于一般可满足性问题不可判定，作者引入局部片段，将量化限制在给定参考点周围、半径有界的邻域内。主要结果包括：在允许一个对角关系时，半径1的局部片段可满足性是可达的；但增大半径会导致不可判定。其次，作者对局部逻辑的存在片段给出了精确的可判定性与复杂度图谱，参数为每个元素携带的数据个数和邻域半径。该工作刻画了适用于带数据系统规约的形式化谱系，并提出了未来研究方向。
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.
@article{paperbot2747,
title = {On the Satisfiability of Local First-Order Logics with Data},
author = {Benedikt Bollig and Arnaud Sangnier and Olivier Stietel},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:1)2024}
}