We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.
翻译:我们定义了一阶逻辑的邻接片段(AF),该片段通过限制原子公式中作为论元出现的变量序列而获得。邻接片段(经常规重命名后)概括了双变量逻辑以及槽形片段。我们证明邻接片段具有有限模型性质,且其可满足性问题不比槽形片段更难(因此是Tower完全的)。我们进一步证明,任何对论元序列中允许的变量顺序的邻接条件的放宽,都会产生一个其可满足性问题和有限可满足性问题均为不可判定的逻辑。最后,我们研究了邻接要求对著名的一阶逻辑有界片段(GF)的影响。我们证明有界邻接片段(GA)的可满足性问题仍是2ExpTime-hard的,从而加强了GF的已知下界。