This paper builds and extends on the authors previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic. First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport \& England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum \& Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an important typo and provide a missing proof in that paper. We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative.

翻译：本文构建并扩展了作者先前关于算法工具——柱形代数分解（CAD）及其核心应用——实量词消去（QE）的研究。这些主题是符号计算的核心，虽然早在数十年前就已首次在计算机代数系统中实现，但近年来随着非线性实算术SMT求解器的持续发展而重新获得关注。首先，我们探讨了传统CAD中迭代单变元结式的使用，以及这如何导致效率低下（尤其是在输入含有多等式约束的情况下）。我们重制了会议论文[Davenport & England, 2023]，对其中首次提出的在CAD投影阶段使用多变元结式的建议进行了重要澄清。随后，我们考察了另一替代方案（最初记载于[McCallum & Brown, 2009]），该方案重新定义了实际构造对象（尽管仅适用于两个等式约束的情形）。我们纠正了该文中的一个重要笔误，并补充了缺失的证明。最后，我们修订了如何处理使用有理函数（而非通常的多项式函数）表达的SMT或实量词消去问题——注意到此类问题常见于工业应用中。我们重新审视了[Uncu, Davenport and England, 2023]中针对可满足性情形提出的方案，阐明了为何该方法难以简单扩展至更复杂的量化结构，并给出了合适的替代方案。