de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

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)$