The First-Order Theory of Ordering Constraints over
Feature Trees
Author: Martin Müller and Joachim Niehren and Ralf Treinen
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. We investigate the first-order theory of FT$_\leq$
and its fragments in detail, both
over finite trees and over possibly infinite trees. We prove that the
first-order theory of FT$_\leq$
is undecidable, in contrast to the first-order theory of FT
which is well-known to be decidable. We show that the entailment
problem of FT$_\leq$ with
existential quantification is PSPACE-complete. So far, this problem
has been shown decidable, coNP-hard in case of finite trees,
PSPACE-hard in case of arbitrary trees, and cubic time when restricted
to quantifier-free entailment judgments. To show PSPACE-completeness,
we show that the entailment problem of FT$_\leq$ with existential
quantification is equivalent to the
inclusion problem of non-deterministic finite automata.
|