de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

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.


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