Deciding Definability in FO_2(<_h, <_v) on Trees
Thomas Place, Luc Segoufin · 2010
We prove that it is decidable whether a regular unranked tree language is definable in FO2(h,v). By FO2(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.