@Article{Müller_et_al:2001,
AUTHOR = {Müller, Martin and Niehren, Joachim and Treinen, Ralf},
TITLE = {The FirstOrder Theory of Ordering Constraints over Feature Trees},
YEAR = {2001},
JOURNAL = {Discrete Mathematics and Theoretical Computer Science},
VOLUME = {4},
NUMBER = {2},
PAGES = {193234},
URL = {ftp://ftp.ps.unisb.de/pub/papers/ProgrammingSysLab/FTSubTheory98.ps.gz},
ABSTRACT = {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 firstorder theory of FT$_leq$ and its fragments in detail, both over finite trees and over possibly infinite trees. We prove that the firstorder theory of FT$_leq$ is undecidable, in contrast to the firstorder theory of FT which is wellknown to be decidable. We show that the entailment problem of FT$_leq$ with existential quantification is PSPACEcomplete. So far, this problem has been shown decidable, coNPhard in case of finite trees, PSPACEhard in case of arbitrary trees, and cubic time when restricted to quantifierfree entailment judgments. To show PSPACEcompleteness, we show that the entailment problem of FT$_leq$ with existential quantification is equivalent to the inclusion problem of nondeterministic finite automata.},
ANNOTE = {COLIURL : Muller:2001:FOT.pdf} }
