相邻片段与 Quine 的决策极限

我们引入第一阶逻辑的相邻片段（AF），通过限制原子公式中变量序列的出现顺序来获得。相邻片段在常规重命名后可概括两变量片段以及所谓的 fluted 片段。我们证明相邻片段具有有限模型属性，其 $k$ 变量子片段的满足性问题在 $(k-1)$-NExpTime 内。利用关于 fluted 片段的已知结果，可得出相邻片段整个的满足性问题为 Tower-complete。我们还额外考虑相邻要求对著名的 guarded 片段的影响，其满足性问题为 TwoExpTime-complete。我们证明相邻片段与 guarded adjacent 片段的交集的满足性问题保持 TwoExpTime-hard。最后，我们证明任何对原子公式中变量顺序的松化都会导致其满足性和有限满足性问题不可判定。