决策的限制：一阶逻辑的相邻片段
摘要：邻接片段AF是一阶逻辑的定义，通过限制原子公式中作为参数出现的变量序列得到。邻接片段推广了两变量逻辑（在常规重命名后）以及有波痕的片段。我们证明邻接片段具有有限模型特性，并且它的可满足性问题不比有波痕片段更困难（因此是Tower-complete）。我们进一步证明，对于允许参数序列中变量顺序的相邻条件的任何放松都会导致逻辑的可满足性和有限可满足性问题不可判定。最后，我们研究了邻接要求对一阶逻辑中广为人知的有保护片段（GF）的影响。我们证明有保护邻接片段（GA）的可满足性问题仍然是2ExpTime-hard，从而加强了GF已知的下界。
作者：Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann
论文ID：2305.03133
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-19