Müller, Martin and Niehren, Joachim and Treinen, Ralf - The First-Order Theory of Ordering Constraints over Feature Trees

dmtcs:267 - Discrete Mathematics & Theoretical Computer Science, January 1, 2001, Vol. 4 no. 2
The First-Order Theory of Ordering Constraints over Feature Trees

Authors: Müller, Martin and Niehren, Joachim and Treinen, Ralf

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


Source : oai:HAL:inria-00536800v1
Volume: Vol. 4 no. 2
Published on: January 1, 2001
Submitted on: March 26, 2015
Keywords: [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO],[INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]


Share

Consultation statistics

This page has been seen 97 times.
This article's PDF has been downloaded 60 times.