MODNET

Research Training Network in Model Theory

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 E-mail: 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: |

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