Tree Languages Defined in First-Order Logic with One Quantifier Alternation
arXiv:1009.2854 · doi:10.2168/LMCS-6(4:1)2010
Abstract
We study tree languages that can be defined in Δ_2 . These are tree languages definable by a first-order formula whose quantifier prefix is forall exists, and simultaneously by a first-order formula whose quantifier prefix is . For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. We provide an effective characterization of tree and forest languages definable in Δ_2 . This characterization is in terms of algebraic equations. Over words, the class of word languages definable in Δ_2 forms a robust class, which was given an effective algebraic characterization by Pin and Weil.
Cited by in corpus (7)
- Piecewise testable tree languages
- A decidable characterization of locally testable tree languages
- Wreath Products of Distributive Forest Algebras
- Deciding definability in FO2(<h,<v) on trees
- Proving that a Tree Language is not First-Order Definable
- Forest languages defined by counting maximal paths
- Quantifier alternation in a class of recursively defined tree properties