The First-Order Theory of Ordering Constraints over Feature Trees - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 1998

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.
Fichier principal
Vignette du fichier
FTSubTheory-Long_99.pdf (326.67 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

inria-00536818 , version 1 (16-11-2010)

Identifiers

  • HAL Id : inria-00536818 , version 1

Cite

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. pp.432--443. ⟨inria-00536818⟩
111 View
75 Download

Share

Gmail Mastodon Facebook X LinkedIn More