Skip to Main content Skip to Navigation
Journal articles

The First-Order Theory of Ordering Constraints over Feature Trees

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. Available at http://www.ps.uni-saarland.de/Publications/documents/FTSubTheory_98.pdf
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/inria-00536800
Contributor : Joachim Niehren <>
Submitted on : Wednesday, June 11, 2014 - 4:46:12 PM
Last modification on : Thursday, July 8, 2021 - 3:48:21 AM
Long-term archiving on: : Thursday, September 11, 2014 - 10:41:28 AM

File

144-411-1-PB.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : inria-00536800, version 1

Collections

Citation

Martin Müller, Joachim Niehren, Ralf Treinen. The First-Order Theory of Ordering Constraints over Feature Trees. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2001, 4 (2), pp.193-234. ⟨inria-00536800⟩

Share

Metrics

Record views

221

Files downloads

872