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.
PostScriptPortable Document Format