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 and 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 and Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an unhelpful typo and provide a proof missing from 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 and England, 2023]的内容，并对其中首次提出的在CAD投影阶段使用多元结式的建议进行了重要澄清。接着，我们考察了[McCallum and Brown, 2009]中首次记载的针对该问题的另一种方法，该方法重新定义了实际构造的对象，尽管仅适用于两个等式约束的情形。我们纠正了原文中一处不利的笔误，并补充了该论文缺失的证明。最后，我们重新探讨了如何处理使用有理函数（而非通常的多项式）表达的SMT或实QE问题，指出此类问题在工业应用中十分常见。我们回顾了[Uncu, Davenport and England, 2023]中针对可满足性情形提出的解决方案，解释了为何该方法不能直接推广到更复杂的量词结构，并给出了合适的替代方案。