SFB 378 Einstiegsseite Postscript File BibTeX Entry

C
NEP

Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic

Author: Martin Müller and Joachim Niehren

Editor:

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_1\models \exists x_1\ldots\exists 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.

SFB 378 Einstiegsseite Postscript File BibTeX Entry