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难度，从而强化了GF的已知下界。