Publication details

Saarland University Computer Science

The First-Order Theory of Ordering Constraints over Feature Trees

Martin Müller, Joachim Niehren, Ralf Treinen

Discrete Mathematics and Theoretical Computer Science 4(2):193-234, 2001

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.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009