User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse





On the decision complexity of the bounded theories of trees


Vorobyov,  Sergei
Programming Logics, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)

(Any fulltext), 16MB

Supplementary Material (public)
There is no public supplementary material available

Vorobyov, S.(1996). On the decision complexity of the bounded theories of trees (MPI-I-1996-2-008). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-9FDF-9
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$.