Deciding Definability In Fo(2)(<(H), <(V)) On Trees

We prove that it is decidable whether a regular unranked tree language is definable in FO(2)(<(h), <(v)). By FO(2)(<(h), <(v)) we refer to the two variable fragment of first order logic built from the descendant and following sibling predicates. In terms of expressive power it corresponds to a fragment of the navigational core of XPath that contains modalities for going up to some ancestor, down to some descendant, left to some preceding sibling, and right to some following sibling.We also investigate definability in some other fragments of XPath.