hide
Free keywords:
-
Abstract:
The first-order theories of finite and rational, constructor and
feature trees possess complete axiomatizations and are decidable by
quantifier elimination [Malcev 61, Kunen 87, Maher 88,
Comon-Lescanne 89, Hodges 93, Backofen-Smolka 92, Smolka-Treinen 92,
Backofen-Treinen94, Backofen95].
By using the uniform inseparability lower bounds techniques due to
[Compton-Henson 90], based on representing
large binary relations by means of short formulas manipulating with
high trees, we prove that all the above theories, as well as all
their subtheories, are NON-ELEMENTARY in the sense of
Kalmar, i.e., cannot be decided within time bounded by a $k$-story
exponential function for any fixed $k$.
Moreover, for some constant $d>0$ these decision problems require
nondeterministic time exceeding $\exp_\infty(dn)$
