Quantifier elimination algorithm to boolean combination of ∃∀-formulas in the theory of a free group

Olga Kharlampovich, Alexei Myasnikov

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

1 Scopus citations

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 languageEnglish
Title of host publicationGroups and Model Theory
Subtitle of host publicationGAGTA BOOK 2
Pages87-125
Number of pages39
ISBN (Electronic)9783110719710
DOIs
StatePublished - 24 May 2021

Fingerprint

Dive into the research topics of 'Quantifier elimination algorithm to boolean combination of ∃∀-formulas in the theory of a free group'. Together they form a unique fingerprint.

Cite this