# Publication details

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

Martin Müller, Joachim Niehren

International Conference on Rewriting Techniques and Applications, Vol. 1379 of Lecture Notes in Computer Science, pp. 196--210, Springer-Verlag, Berlin, 1998

The system FT$_lt$ of ordering constraints over feature trees has been introduced as an extension of the system FT of equality constraints
over feature trees. We investigate decidability and complexity questions
for fragments of the first-order theory of FT$_lt$. It is well-known that
the first-order theory of FT$_lt$ is decidable and that several of its
fragments can be decided in quasi-linear time, including the
satisfiability problem of FT$_lt$ and its entailment problem
with existential quantification
$$phimodels E x1 ... E xn ( phi' )$$
Much less is known on the first-order theory
of FT$_lt$. The satisfiability problem of FT$_lt$ can be decided in cubic
time, as well as its entailment problem without existential
quantification. Our main result is that the entailment
problem of FT$_lt$ with existential quantifiers is
decidable but PSPACE-hard. Our decidability proof is based on a
new technique where feature constraints are expressed in second-order
monadic logic with countably many successors SwS. We thereby reduce
the entailment problem of FT$_lt$ with existential quantification
to Rabin's famous theorem on tree automata.

Download PDF
Show BibTeX

@INPROCEEDINGS{MuellerNiehren:SWS:9,
title = {Ordering Constraints over Feature Trees Expressed in Second-order Monadic Logic},
author = {Martin Müller and Joachim Niehren},
year = {1998},
editor = {{Tobias Nipkow}},
publisher = {{Springer-Verlag, Berlin}},
booktitle = {International Conference on Rewriting Techniques and Applications},
series = {{Lecture Notes in Computer Science}},
volume = {{1379}},
pages = {{196--210}},
address = {{Tsukuba, Japan}},
}

Login to edit

Legal notice, Privacy policy