## Paper: The First-Order Theory of Ordering Constraints over Feature Trees (at LICS 1998)

**Martin Müller Joachim Niehren Ralf Treinen**

### 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, 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 determine the complexity
of the entailment problem of FT_{⩽} with existential
quantification to be PSPACE-complete, by proving its equivalence to the
inclusion problem of non-deterministic finite automata. Our reduction
from the entailment problem to the inclusion problem is based on a new
algorithm that, given an existential formula of FT_{⩽},
computes a finite automaton which accepts all its logic consequences

### BibTeX

@InProceedings{MllerNiehrenTreinen-TheFirstOrderTheory, author = {Martin Müller and Joachim Niehren and Ralf Treinen}, title = {The First-Order Theory of Ordering Constraints over Feature Trees}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {432--443}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }