# Publication details

##
The First-Order Theory of Ordering Constraints over Feature Trees

Martin Müller, Joachim Niehren, Ralf Treinen

Discrete Mathematics and Theoretical Computer Science 4(2):193-234, 2001

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.

Download PDF
Show BibTeX

@ARTICLE{FTSubTheory-Long:99,
title = {The First-Order Theory of Ordering Constraints over Feature Trees},
author = {Martin M{\"u}ller and Joachim Niehren and Ralf Treinen},
year = {2001},
journal = {{Discrete Mathematics and Theoretical Computer Science}},
volume = {4},
pages = {{193-234}},
number = {2},
}

Login to edit

Legal notice, Privacy policy