@InProceedings{Müller_Niehren:1998,
AUTHOR = {Müller, Martin and Niehren, Joachim},
TITLE = {Ordering Constraints over Feature Trees Expressed in SecondOrder Monadic Logic},
YEAR = {1998},
BOOKTITLE = {9th International Conference on Rewriting Techniques and Applications (RTA '98), March 30  April 1},
NUMBER = {1379},
PAGES = {196210},
EDITOR = {Nipkow, T.},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Tsukuba, Japan},
PUBLISHER = {SpringerVerlag},
URL = {ftp://ftp.ps.unisb.de/pub/papers/ProgrammingSysLab/SWS97.ps.gz},
ABSTRACT = {The system FT$_lt$ of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints over feature trees. We investigate decidability and complexity questions for fragments of the firstorder theory of FT$_lt$. It is wellknown that the firstorder theory of FT$_lt$ is decidable and that several of its fragments can be decided in quasilinear time, including the satisfiability problem of FT$_lt$ and its entailment problem with existential quantification $$phimodels E x1 ... E xn ( phi' )$$ Much less is known on the firstorder theory of FT$_lt$. The satisfiability problem of FT$_lt$ can be decided in cubic time, as well as its entailment problem without existential quantification. Our main result is that the entailment problem of FT$_lt$ with existential quantifiers is decidable but PSPACEhard. Our decidability proof is based on a new technique where feature constraints are expressed in secondorder monadic logic with countably many successors SwS. We thereby reduce the entailment problem of FT$_lt$ with existential quantification to Rabin's famous theorem on tree automata.},
ANNOTE = {COLIURL : Muller:1998:OCF.pdf Muller:1998:OCF.ps} }
