## Term Algebras with Length Function and Bounded Quantifier Alternation

Ting Zhang,
Henny Sipma,
Zohar Manna.
Term algebras have wide applicability in computer science.
Unfortunately, the decision problem for term algebras has a
nonelementary lower bound, which makes the theory and any extension of
it intractable in practice. However, it is often
more appropriate to consider the *bounded class*, in which
formulae can have arbitrarily long sequences of quantifiers but the
quantifier alternation depth is bounded. In this paper we present new
quantifier elimination procedures for the first-order theory of term
algebras and for its extension with integer arithmetic. The
elimination procedures deal with a block of quantifiers of the same
type in one step. We show that for the bounded class of at most k
quantifier alternations, regardless of the total number of
quantifiers, the complexity of our procedures is k-fold exponential
(resp. 2k fold exponential) for the theory of term algebras
(resp. for the extended theory with integers).

In the *17th Internation Conference on Theorem Proving in Higher Order
Logics (TPHOLS'04)*, LNCS 3223, pp 321-336, Springer Verlag 2004.

BibTex,
Postscript,
PDF (Extended version).
© 2004, Springer Verlag.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: April 7 14:40:50 PDT 2005