max planck institut
informatik

# 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

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:

96-2-008.pdf37 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},