An improved lower bound for the elementary theories of trees

Vorobyov, Sergei

doi:10.1007/3-540-61511-3_91

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

An improved lower bound for the elementary theories of trees

MPS-Authors

/persons/resource/persons45677

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

External Resource

https://rdcu.be/dttRa
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

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: https://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)$