Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic

AbstractThe language FT⩽ of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints over feature trees. While the first-order theory of FT is well understood, only few decidability results are known for the first-order theory of FT⩽. We introduce a new method for proving the decidability of fragments of the first-order theory of FT⩽. This method is based on reduction to second order monadic logic that is decidable according to Rabin's famous tree theorem. The method applies to any fragment of the first-order theory of FT⩽ for which one can change the model towards sufficiently labeled feature trees—a class of trees that we introduce. As we show, the first order-theory of ordering constraints over sufficiently labeled feature trees is equivalent to second-order monadic logic (S2S for infinite and WS2S for finite feature trees). We apply our method for proving that entailment of FT⩽ with existential quantifiers ϕ1⊨∃x1…∃xnϕ2 is decidable. Previous results were restricted to entailment without existential quantifiers which can be solved in cubic time. Meanwhile, entailment with existential quantifiers has been shown to be PSPACE-complete (for finite and infinite feature trees, respectively)