de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

On the bounded theories of finite trees

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


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