Submission date: 10 July 2012.

Abstract:

This paper is written as an appendix to the paper “Elementary theory of free non-abelian groups” by the authors. We are planning to produce more self-contained version later. arXiv admin note: substantial text overlap with arXiv:1111.0577

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.

Mathematics Subject Classification: 20E05, 03CXX

Keywords and phrases:

Full text arXiv 1207.1900: pdf, ps.