Deciding definability in FO2(<h,<v) on trees

Thomas Place, Luc Segoufin

We provide a decidable characterization of regular forest languages definable in FO2(<h,<v). By FO2(<h,<v) we refer to the two variable fragment of first order logic built from the…