Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

An improved lower bound for the elementary theories of trees


Vorobyov,  Sergei
Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Vorobyov, S. (1996). An improved lower bound for the elementary theories of trees. In M. A. McRobbie, & J. K. Slaney (Eds.), Proceedings of the 13th International Conference on Automated Deduction (CADE-13) (pp. 275-287). Berlin, Germany: Springer.

Cite as:
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)$