% % GENERATED FROM https://www.coli.uni-saarland.de % by : anonymous % IP : coli2006.lst.uni-saarland.de % at : Mon, 05 Feb 2024 15:43:16 +0100 GMT % % Selection : Reference #884 % @Article{Müller_Niehren:2000, AUTHOR = {Müller, Martin and Niehren, Joachim}, TITLE = {Ordering Constraints over Feature Trees Expressed in Second-Order Monadic Logic}, YEAR = {2000}, JOURNAL = {Information and Computation}, VOLUME = {159}, NUMBER = {1-2}, PAGES = {22-58}, URL = {ftp://ftp.ps.uni-sb.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 first-order theory of FT is well understood, only few complexity and decidability results are known for fragments of the first-order theory of FT$_leq$. We introduce a new handle for such decidability questions by showing how to express ordering constraints over feature trees in second-order 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 PSPACE-hard even though the quantifier-free case can be solved in cubic time. To our knowledge, this is the first time that a non-trivial decidability result of feature logic is reduced to Rabins famous tree theorem.}, ANNOTE = {COLIURL : Muller:2000:OCFa.pdf Muller:2000:OCFa.ps} }