关于具有数据的局部一阶逻辑的可满足性
摘要：对于具有无限域中有限数量的数据值的无序结构，我们研究一阶逻辑。数据值可以通过等式进行比较。由于这种逻辑的可满足性问题通常是不可判定的，我们引入了一族局部片段。它们将量化限制在以某个半径为界的给定参考点的邻域内。我们的第一个主要结果是，在存在一个"对角线关系"的情况下，局部半径为1的片段的可满足性问题是可判定的。另一方面，增加半径会导致不可判定性。在第二部分中，我们提供了局部逻辑存在性片段的可满足性问题的精确可判定性和复杂性情况。这些片段的参数是每个元素携带的数据值数量和所考虑邻域的半径。总的来说，我们绘制了适用于具有数据的系统规范的形式化方法的情景，并为未来的研究开辟了新的途径。
作者：Benedikt Bollig and Arnaud Sangnier and Olivier Stietel
论文ID：2307.00831
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-04