de.mpg.escidoc.pubman.appbase.FacesBean
English

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### On the bounded theories of finite trees

##### MPS-Authors
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;

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

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: http://hdl.handle.net/11858/00-001M-0000-0014-ABF4-7
##### Abstract
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$.