author: | Martin Müller and Joachim Niehren and Ralf Treinen |
title: | The first-order theory of ordering constraints over feature trees |
keywords: | feature constraints, logic of trees, automata |
abstract: | 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. We investigate the first-order
theory of FT≤ and its fragments in detail, both over finite
trees and over possibly infinite trees. We prove that the
first-order theory of FT≤ 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≤ 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≤ with existential
quantification is equivalent to the inclusion problem of
non-deterministic finite automata.
|
reference: |
Martin Müller and Joachim Niehren and Ralf Treinen (2001),
The first-order theory of ordering constraints over feature trees ,
Discrete Mathematics and Theoretical Computer Science 4, pp. 193-234 |
ps.gz-source: | dm040211.ps.gz (150 K) |
ps-source: | dm040211.ps (572 K) |
pdf-source: | Unfortunately it was not possible to produce a PDF version due to TeXnichal incompatibilities. |