One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential (universal) quantifiers that leave at most one variable free. We investigate this fragment over words and trees, presenting a complete classification of the complexity of its satisfiability problem for various navigational signatures, and comparing its expressive power with other important formalisms. These include the two-variable fragment with counting and the unary negation fragment.
翻译:将一阶逻辑的一维碎片限制在最多一个变量的存续(通用)量化符。 我们用文字和树木来调查这一碎片,对各种导航签字的可相对性问题的复杂性进行完整分类,并将它与其他重要形式主义的表达力进行比较。 其中包括两个变量的点数碎片和不完全否定的碎片。