Research Training Network in Model Theory
Publications > Preprint server > Preprint Number 478

Preprint Number 478

Previous Next Preprint server

478. Olga Kharlampovich, Alexei Myasnikov
Quantifier elimination algorithm to boolean combination of \exists\forall-formulas in the theory of a free group

Submission date: 10 July 2012.


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.

Last updated: July 13 2012 16:21 Please send your corrections to: