The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime{}-complete satisfiability.

翻译：一阶逻辑的均匀一维片段于数年前被提出，作为两变量片段在处理元数大于二的关系语境下的推广。该逻辑中的量词以块的形式使用，每个块仅包含存在量词或仅包含全称量词。本文探讨在量词块中混合两种类型量词的可能性。我们证明了所得形式化体系的两种限制具有有限（指数）模型性质且可满足性问题为NExpTime完全：第一种限制要求每个量词块要么为纯全称量词，要么以存在量词结尾；第二种限制将变量数量限定为三个；两种情形均不允许等词。我们还将第二种变体扩展至三变量片段（无等词）的一个丰富子片段，该子片段仍保持有限模型性质，且具有可判定的、NExpTime完全的满足性问题。