de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

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

##### MPG-Autoren
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;

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

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.

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