Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要