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.