Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  On the Bounded Theories of Finite Trees

Vorobyov, S. (1996). On the Bounded Theories of Finite Trees. In J. Jaffar, & R. H. C. Yap (Eds.), Concurrency and Parallelism, Programming, Networking, and Security (pp. 152-161). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-ABF4-7 Versions-Permalink: https://hdl.handle.net/21.11116/0000-000E-398F-2
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
https://rdcu.be/dv1a4 (Verlagsversion)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

einblenden:
ausblenden:
 Urheber:
Vorobyov, Sergei1, 2, Autor           
Affiliations:
1Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society, ou_40046              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 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$.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121996
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519642
Anderer: Local-ID: C1256104005ECAFC-F79A9507CD9D39E4C12564570040AE2A-Vorobyov96ASIAN96
BibTex Citekey: Vorobyov_ASIAN96
DOI: 10.1007/BFb0027788
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Second Asian Computing Science Conference
Veranstaltungsort: Singapore
Start-/Enddatum: 1996-12-02 - 1996-12-05

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Concurrency and Parallelism, Programming, Networking, and Security
  Untertitel : Second Asian Computing Science Conference ASIAN'96
  Kurztitel : ASIAN 1996
Genre der Quelle: Konferenzband
 Urheber:
Jaffar, Joxan1, Herausgeber
Yap, Roland H. C.1, Herausgeber
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 152 - 161 Identifikator: ISBN: 978-3-540-62031-0

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 1179 Artikelnummer: - Start- / Endseite: - Identifikator: -