Quantifier Elimination in Term Algebras
Thomas Sturm and Volker Weispfenning
Abstract.
We give a quantifier elimination procedure for term algebras over
suitably expanded finite first-order languages. Our expansion is
purely functional. Our method works by substituting finitely many
parametric test terms. This allows us to obtain in addition sample
solutions for an outermost existential quantifier block. The existence
of our method implies that the considered quantifier elimination
problem and as well the corresponding decision problem are in the
fourth Grzegorcyk complexity class. For prenex input formulas with a
bounded number of quantifiers our quantifier elimination procedure is
elementary recursive. The same applies to arbitrary input formulas in
case the language has only constants and unary function symbols. As a
corollary we get corresponding upper bounds for the decision problem
for term algebras.