joint work with Witold Charatonik and Emanuel Kieroński

We consider the satisfiability problem for the two-variable fragment
of first-order logic over finite unranked trees. We work with
signatures consisting of some unary predicates and the binary
navigational predicates child, right sibling, and their respective
transitive closures. We prove that the satisfiability problem for the
logic containing all these predicates is EXPSPACE-complete.

Further, we consider the restriction of the class of structures to
singular trees, i.e., we assume that at every node precisely one unary
predicate holds. We observe that most logics, even if we work on
unordered trees, remain EXPSPACE-complete over finite singular trees,
but the complexity decreases for some weaker logics. Namely, the logic
with one binary predicate, ancestor, is NEXPTIME-complete, and its
guarded version is PSPACE-complete over finite singular trees, even
though both these logics are EXPSPACE-complete over arbitrary finite
trees.