Publications > Preprint server > Preprint Number 478
Preprint Number 478
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:
|Last updated: July 13 2012 16:21||Please send your corrections to:|