# MPI-I-96-2-008

## On the decision complexity of the bounded theories of trees

### Vorobyov, Sergei

**MPI-I-96-2-008**. November** **1996, 26 pages. | Status:** **available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

The theory of finite trees is the full first-order theory of

equality in the Herbrand universe (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 [Vorobyov CADE'96].

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

Acknowledgement:** **

References to related material:

To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |

96-2-008.pdf | 37 KBytes; 133 KBytes; 15957 KBytes |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |

**URL to this document: **http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1996-2-008

**BibTeX**
`@TECHREPORT{``Vorobyov96-RR-008``,`

` AUTHOR = {Vorobyov, Sergei},`

` TITLE = {On the decision complexity of the bounded theories of trees},`

` TYPE = {Research Report},`

` INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},`

` ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},`

` NUMBER = {MPI-I-96-2-008},`

` MONTH = {November},`

` YEAR = {1996},`

` ISSN = {0946-011X},`

`}`