Quantifier elimination algorithm to boolean combination of $\exists\forall$-formulas in the theory of a free group
Group Theory
2019-09-13 v4
Abstract
It was proved by Sela and by the authors that every formula in the theory of a free group is equivalent to a boolean combination of -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 ). In this paper we give an algorithm for reduction of a first order formula over a free group to an equivalent boolean combination of -formulas.
Keywords
Cite
@article{arxiv.1207.1900,
title = {Quantifier elimination algorithm to boolean combination of $\exists\forall$-formulas in the theory of a free group},
author = {Olga Kharlampovich and Alexei Myasnikov},
journal= {arXiv preprint arXiv:1207.1900},
year = {2019}
}
Comments
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