  |
Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic
Autor: Martin Müller and Joachim NiehrenHerausgeber: Tobias Nipkow
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 first-order theory of FT$_\lt$. It is well-known that
the first-order theory of FT$_\lt$ is decidable and that several of its
fragments can be decided in quasi-linear time, including the
satisfiability problem of FT$_\lt$ and its entailment problem
with existential quantification
$$\phi\models E\ x1 ... E\ xn ( \phi' )$$
Much less is known on the first-order 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 PSPACE-hard. Our decidability proof is based on a
new technique where feature constraints are expressed in second-order
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.
|