%
% GENERATED FROM https://www.coli.uni-saarland.de
%    by   : anonymous
%    IP   : coli2006.lst.uni-saarland.de
%    at   : Mon, 05 Feb 2024 15:43:27 +0100 GMT
%    
% Selection : Reference #888
%




@InProceedings{Müller_et_al:1998,
      AUTHOR = {Müller, Martin and Niehren, Joachim and Treinen, Ralf},
      TITLE = {The First-Order Theory of Ordering Constraints over Feature Trees},
      YEAR = {1998},
      BOOKTITLE = {13th Annual IEEE Symposium on Logic in Computer Sience (LICS '98), June 21 - 24},
      PAGES = {432-443},
      ADDRESS = {Indianapolis, Indiana, USA},
      PUBLISHER = {IEEE Press},
      URL = {http://www.ps.uni-sb.de/Papers/abstracts/FTSubTheory-Long:99.html ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/FTSubTheory-Long:99.ps.gz},
      ABSTRACT = {The system FT$_leq$ 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$_leq$ and its fragments in detail, both over finite trees and over possibly infinite trees. We prove that the first-order theory of FT$_leq$ 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$_leq$ 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$_leq$ with existential quantification is equivalent to the inclusion problem of non-deterministic finite automata.},
      ANNOTE = {COLIURL : Muller:1998:FOT.pdf Muller:1998:FOT.ps}
}