Proceedings Article, Paper @InProceedings Beitrag in Tagungsband, Workshop

 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 Author, Editor
 Author(s): Vorobyov, Sergei dblp
 Editor(s): Jaffar, Joxan Yap, Roland H. C. dblp dblp
 BibTeX cite key*: Vorobyov96ASIAN96

 Title, Booktitle
 Title*: On the bounded theories of finite trees Booktitle*: Second Asian Computing Science Conference, ASIAN'96

 Event, URLs
 URL of the conference: URL for downloading the paper: Event Address*: Singapore Language: English Event Date* (no longer used): December 2-5, 1996 Organization: Event Start Date: 21 November 2019 Event End Date: 21 November 2019

 Publisher
 Name*: Springer URL: Address*: Berlin, Germany Type: Full paper

 Vol, No, Year, pp.
 Series: Lecture Notes in Computer Science
 Volume: 1179 Number: Month: Pages: 152-161 Year*: 1996 VG Wort Pages: ISBN/ISSN: 3-540-62031-1 Sequence Number: DOI:

 (LaTeX) 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$. Keywords: Decision complexity of logical theories Download Access Level:

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@INPROCEEDINGS{Vorobyov96ASIAN96,
AUTHOR = {Vorobyov, Sergei},
EDITOR = {Jaffar, Joxan and Yap, Roland H. C.},
TITLE = {On the bounded theories of finite trees},
BOOKTITLE = {Second Asian Computing Science Conference, ASIAN'96},
PUBLISHER = {Springer},
YEAR = {1996},
TYPE = {Full paper},
VOLUME = {1179},
PAGES = {152--161},
SERIES = {Lecture Notes in Computer Science},