Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

An improved lower bound for the elementary theories of trees

MPG-Autoren
/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

https://rdcu.be/dttRa
(Verlagsversion)

Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe 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: https://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)$