Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic

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. While the first-order theory of FT is well understood, only few complexity and decidability results are known for fragments of the first-order theory of FT<. We introduce a new handle for such decidability questions by showing how to express ordering constraints over feature trees in second-order monadic logic (S2S or WS2S). Our relationship implies a new decidability result for feature logics, namely that the entailment problem of FT< with existential quantifiers P |= models exists x1 ... exists xn P' is decidable. We also show that this problem is PSPACE-hard even though the quantifier-free case can be solved in cubic time. To our knowledge, this is the first time that a non-trivial decidability result of feature logic is reduced to Rabins famous tree theorem.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2000, 159 (1/2), pp.22--58
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00536798
Contributeur : Joachim Niehren <>
Soumis le : mardi 16 novembre 2010 - 23:08:58
Dernière modification le : mardi 31 octobre 2017 - 14:22:18
Document(s) archivé(s) le : jeudi 17 février 2011 - 03:12:59

Fichiers

SWSJournal99.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00536798, version 1

Citation

Martin Müller, Joachim Niehren. Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic. Information and Computation, Elsevier, 2000, 159 (1/2), pp.22--58. 〈inria-00536798〉

Partager

Métriques

Consultations de la notice

65

Téléchargements de fichiers

59