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.
Type de document :
Communication dans un congrès
13th annual IEEE Symposium on Logic in Computer Sience, 1998, Indianapolis, Indiana, United States. IEEE Computer Science Press, pp.432--443, 1998
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00536818
Contributeur : Joachim Niehren <>
Soumis le : mardi 16 novembre 2010 - 23:10:29
Dernière modification le : jeudi 11 janvier 2018 - 06:20:11
Document(s) archivé(s) le : jeudi 17 février 2011 - 03:16:12

Fichiers

FTSubTheory-Long_99.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00536818, version 1

Collections

Citation

Martin Müller, Joachim Niehren, Ralf Treinen. The First-Order Theory of Ordering Constraints over Feature Trees. 13th annual IEEE Symposium on Logic in Computer Sience, 1998, Indianapolis, Indiana, United States. IEEE Computer Science Press, pp.432--443, 1998. 〈inria-00536818〉

Partager

Métriques

Consultations de la notice

128

Téléchargements de fichiers

46