Müller, Martin; Niehren, Joachim; Treinen, Ralf The first-order theory of ordering constraints over feature trees. (English) Zbl 0981.68081 Discrete Math. Theor. Comput. Sci. 4, No. 2, 193-234 p. (2001). Summary: The system \(FT_\leq\) of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints over feature trees. We investigate the first-order theory of \(FT_\leq\) and its fragments in detail, both over finite trees and over possibly infinite trees. We prove that the first-order theory of \(FT_\leq\) is undecidable, in contrast to the first-order theory of FT which is well-known to be decidable. We show that the entailment problem of \(FT_\leq\) with existential quantification is PSPACE-complete. So far, this problem has been shown decidable, coNP-hard in case of finite trees, PSPACE-hard in case of arbitrary trees, and cubic time when restricted to quantifier-free entailment judgments. To show PSPACE-completeness, we show that the entailment problem of \(FT_\leq\) with existential quantification is equivalent to the inclusion problem of non-deterministic finite automata. MSC: 68Q45 Formal languages and automata Keywords:feature constraints; logic of trees; automata Software:Oz PDFBibTeX XMLCite \textit{M. Müller} et al., Discrete Math. Theor. Comput. Sci. 4, No. 2, 193--234 p. (2001; Zbl 0981.68081) Full Text: EuDML EMIS