Iterated Resultants and Rational Functions in Real Quantifier Elimination

TL;DR

The paper advances CAD-based real quantifier elimination by clarifying the role of iterated univariate resultants, introducing multivariate resultants for projection, and refining equational-constraint strategies to reduce spurious factors. It provides corrected theorems and proofs for delineability with multiple equational constraints, and extends the framework to rational-function inputs by modeling restricted domains and domain-aware quantification. The work analyzes degree-growth implications, proposes practical heuristics to detect spurious factors, and outlines future directions toward generalized projections and CAD variants. Overall, the methods aim to improve the scalability and applicability of QE/SMT approaches to non-linear real arithmetic in industrial contexts.

Abstract

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.

Theorems & Definitions (14)

• Example
• Remark 2.1
• Definition 2.2
• Proposition 2.3
• Proposition 2.4
• Proposition 2.5
• Definition 4.1
• Remark 4.2
• Example
• Theorem 5.1: McCallumBrown2009