自由群理论中公式到 $\exists\forall$-公式布尔组合的量词消去算法
群论
2019-09-13 v4
摘要
Sela 和作者证明了自由群 理论中的每个公式等价于 -公式的布尔组合。我们还证明了自由群的初等理论是可判定的（存在一个算法，给定一个语句，判断该语句是否属于 ）。本文给出了将自由群上的一阶公式归约为等价 -公式布尔组合的算法。
引用
@article{arxiv.1207.1900,
title = {Quantifier elimination algorithm to boolean combination of $\exists\forall$-formulas in the theory of a free group},
author = {Olga Kharlampovich and Alexei Myasnikov},
journal= {arXiv preprint arXiv:1207.1900},
year = {2019}
}
备注
In this version we describe in more details the algorithm from our paper "Elementary theory of free non-abelian groups" (J. Algebra, 302, 2006). We also corrected some misprints and non-essential errors in "Elementary theory of free non-abelian groups" noticed by different people