de.mpg.escidoc.pubman.appbase.FacesBean
English

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### An improved lower bound for the elementary theories of trees

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45677

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

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

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: http://hdl.handle.net/11858/00-001M-0000-0014-ABC5-F
##### 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)$