Quantifier elimination algorithm to boolean combination of $\exists\forall$-formulas in the theory of a free group

DOI10.1515/9783110719710-003arXiv1207.1900MaRDI QIDQ6234234

Alexei Myasnikov, Olga Kharlampovich

Publication date: 8 July 2012

Abstract: 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 $existsforall$-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 $existsforall$-formulas.

Mathematics Subject Classification ID

Applications of logic to group theory (20A15) Model-theoretic algebra (03C60) Decidability of theories and sets of sentences (03B25) Free nonabelian groups (20E05) Quantifier elimination, model completeness, and related topics (03C10)

This page was built for publication: Quantifier elimination algorithm to boolean combination of $\exists\forall$-formulas in the theory of a free group

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6234234)