Quantifier elimination algorithm to boolean combination of $\exists \forall$-formulas in the theory of a free group

Abstract

It was proved by Sela and by the authors that every formula in the theory of a free group $F$ is equivalent to a boolean combination of $\exists \forall$-formulas. We also proved that the elementary theory of a free group is decidable (there is an algorithm given a sentence to decide whether this sentence belongs to $Th(F)$). In this paper we give an algorithm for reduction of a first order formula over a free group to an equivalent boolean combination of $\exists \forall$-formulas.

In this version we describe in more details the algorithm from our paper "Elementary theory of free non-abelian groups" (J. Algebra, 302, 2006). We also corrected some misprints and non-essential errors in "Elementary theory of free non-abelian groups" noticed by different people

References in corpus (1)

• Strong accessibility for finitely presented groups

Cited by in corpus (2)

• Decidability of the Elementary Theory of a Torsion-Free Hyperbolic Group
• On Tarski's Decidability Problem