Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

On the bounded theories of finite trees


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

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Vorobyov, S. (1996). On the bounded theories of finite trees. In J. Jaffar, & R. H. C. Yap (Eds.), Second Asian Computing Science Conference, ASIAN'96 (pp. 152-161). Berlin, Germany: Springer.

Cite as:
The theory of finite trees is the full first-order theory of equality in the Herbrand universum (the set of ground terms) over a functional signature containing non-unary function symbols and constants. Albeit decidable, this theory turns out to be of non-elementary complexity [Vorobyov96CADE96]. To overcome the intractability of the theory of finite trees, we introduce in this paper the bounded theory of finite trees. This theory replaces the usual equality $=$, interpreted as identity, with the infinite family of approximate equalities ``down to a fixed given depth'' $\{=^d\}_{d\in\omega}$, with $d$ written in binary notation, and $s=^dt$ meaning that the ground terms $s$ and $t$ coincide if all their branches longer than $d$ are cut off. By using a refinement of Ferrante-Rackoff's complexity-tailored Ehrenfeucht-Fraisse games, we demonstrate that the bounded theory of finite trees can be decided within linear double exponential space $2^{2^{cn}}$ ($n$ is the length of input) for some constant $c>0$.