Ordering Constraints over Feature Trees Expressed in
Second-order Monadic Logic
Author: Martin Müller and Joachim Niehren
Editor:
The system FT
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.
|