Caviness, B. F. 和 Johnson, J. R. (编辑). 量词消去与柱形代数分解。 纽约：Springer-Verlag，1998 年。Collins, G. E. “通过柱形代数分解对实闭域进行量词消去。” 在第二届 GI 计算机自动机理论与形式语言会议论文集中。纽约：Springer-Verlag，第 134-183 页，1975 年。Collins, G. E. “通过柱形代数分解进行量词消去——二十年的进展。” 在量词消去与柱形代数分解（B. F. Caviness 和 J. R. Johnson 编辑）中。纽约：Springer-Verlag，第 8-23 页，1998 年。Collins, G. E. 和 Hong, H. “用于量词消去的部分柱形代数分解。” J. Symb. Comput.12, 299-328, 1991 年。Davenport, J. H. “柱形代数分解的计算机代数。” 报告 TRITA-NA-8511，NADA，KTH，斯德哥尔摩，1985 年 9 月。Davenport, J. 和 Heintz, J. “实数量词消去是双重指数级的。” J. Symb. Comput.5, 29-35, 1988 年。Dolzmann, A. 和 Sturm, T. “有序域上无量词公式的简化。” J. Symb. Comput.24, 209-231, 1997 年。Dolzmann, A. 和 Weispfenning, V. “局部量词消去。” http://www.fmi.uni-passau.de/~dolzmann/refs/MIP-0003.ps.Z。Heintz, J.; Roy, R.-F.; 和 Solerno, P. “Tarski-Seidenberg 原理的复杂度。” C. R. Acad. Sci. Paris Sér. I Math.309, 825-830, 1989 年。Loos, R. 和 Weispfenning, V. “应用格量词消去。” Comput. J.36, 450-461, 1993 年。Strzebonski, A. “求解代数不等式。” Mathematica J.7, 525-541, 2000 年。Weispfenning, V. “域中线性问题的复杂度。” J. Symb. Comput.5, 3-27, 1988 年。
和 存在量词 
）。如果对于每个量化公式，都存在一个等效的无量词公式，则一阶理论允许量词消去。 这些理论的例子包括带有 
、
、
和 
的实数理论，以及带有 
、
和 
的复数理论。 量词消去在以下工具中实现为解决[expr]。