English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  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.), Second Asian Computing Science Conference, ASIAN'96 (pp. 152-161). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Vorobyov, Sergei1, 2, Author           
Affiliations:
1Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society, ou_40046              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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$.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121996
 Publication Status: Issued
 Pages: -
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519642
Other: Local-ID: C1256104005ECAFC-F79A9507CD9D39E4C12564570040AE2A-Vorobyov96ASIAN96
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Singapore
Start-/End Date: 1996

Legal Case

show

Project information

show

Source 1

show
hide
Title: Second Asian Computing Science Conference, ASIAN'96
Source Genre: Proceedings
 Creator(s):
Jaffar, Joxan, Editor
Yap, Roland H. C., Editor
Affiliations:
-
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 152 - 161 Identifier: ISBN: 3-540-62031-1

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -