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 |