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

TL;DR

This paper presents a decidable method for characterizing which regular forest languages can be defined using a specific two-variable first-order logic fragment with descendant and sibling relations, relevant for XPath-like queries.

Contribution

It provides a decidable characterization of FO2(<h,<v) definability on trees and extends techniques to other similar two-variable logics with different horizontal modalities.

Findings

Decidable characterization of FO2(<h,<v) definability on trees

Techniques applicable to other two-variable logics with similar vertical modalities

Enhanced understanding of the expressive power of XPath fragments

Abstract

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 descendant relation and the following sibling relation. 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 show that our techniques can be applied to other two variable first-order logics having exactly the same vertical modalities as FO2(<h,<v) but having different horizontal modalities.