Abstract
It was proved by Sela and by the authors that every formula in the theory of a nonabelian free group F 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 Th(F). Here we describe an algorithm for the reduction of a first-order formula over a free group to the equivalent boolean combination of ∃∀-formulas.
| Original language | English |
|---|---|
| Title of host publication | Groups and Model Theory |
| Subtitle of host publication | GAGTA BOOK 2 |
| Pages | 87-125 |
| Number of pages | 39 |
| ISBN (Electronic) | 9783110719710 |
| DOIs | |
| State | Published - 24 May 2021 |