@Article{Müller_Niehren:2000,
AUTHOR = {Müller, Martin and Niehren, Joachim},
TITLE = {Ordering Constraints over Feature Trees Expressed in SecondOrder Monadic Logic},
YEAR = {2000},
JOURNAL = {Information and Computation},
VOLUME = {159},
NUMBER = {12},
PAGES = {2258},
URL = {ftp://ftp.ps.unisb.de/pub/papers/ProgrammingSysLab/SWSJournal99.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. While the firstorder theory of FT is well understood, only few complexity and decidability results are known for fragments of the firstorder theory of FT$_leq$. We introduce a new handle for such decidability questions by showing how to express ordering constraints over feature trees in secondorder monadic logic (S2S or WS2S). Our relationship implies a new decidability result for feature logics, namely that the entailment problem of FT$_leq$ with existential quantifiers $phi_1models exists x_1ldotsexists x_n phi_2$ is decidable. We also show that this problem is PSPACEhard even though the quantifierfree case can be solved in cubic time. To our knowledge, this is the first time that a nontrivial decidability result of feature logic is reduced to Rabins famous tree theorem.},
ANNOTE = {COLIURL : Muller:2000:OCFa.pdf Muller:2000:OCFa.ps} }
