de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

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$.