One-Dimensional Fragment over Words and Trees

TL;DR

This paper studies a specific fragment of first-order logic over words and trees, classifying the complexity of its satisfiability problem and comparing its expressive power with other logical formalisms.

Contribution

It provides a complete complexity classification for the satisfiability problem of the one-dimensional fragment over words and trees, and compares its expressive power with related logics.

Findings

Complexity classifications for various signatures

Comparison with two-variable fragment with counting

Comparison with unary negation fragment

Abstract

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.