Iterated Resultants and Rational Functions in Real Quantifier Elimination

James H. Davenport; Matthew England; Scott McCallum; Ali Uncu

doi:10.1007/s11786-025-00606-4

Iterated Resultants and Rational Functions in Real Quantifier Elimination

James H. Davenport
, Matthew England
, Scott McCallum
, Ali Uncu

Research Centre for Computational Science and Mathematical Modelling

University of Bath
Macquarie University
Australian Academy of Sciences

Research output: Contribution to journal › Article › peer-review

7 Downloads (Pure)

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 & 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 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.

Original language	English
Article number	12
Number of pages	23
Journal	Mathematics in Computer Science
Volume	19
DOIs	https://doi.org/10.1007/s11786-025-00606-4
Publication status	Published - 19 Nov 2025

Bibliographical note

© The Author(s) 2025.
This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original
author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. CC BY

Funding

JHD, ME and AKU are supported by the UK’s EPSRC, via the DEWCAD Project, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (grant numbers EP/T015713/1 and EP/T015748/1), as was SMcC’s visit to the UK to work with JHD and ME. AKU also acknowledges the support of Austrian Science Fund (FWF) project P3401-N. The authors are grateful to Jasper Nalbach whose questions about [] led us to provide the clarification in Section and the new Section ; and to Chris Brown and Zoltan Kovács whose conversation prompted Section . We are also grateful to Gregory Sankaran, Tereso del Río and Amirhosein Sadeghi Manesh for useful conversations on equational constraints. Finally, we express our gratitude to the anonymous referees whose comments greatly improved the final version of this paper.

Funders	Funder number
Engineering and Physical Sciences Research Council	EP/T015713/1 , EP/T015748/1
Austrian Science Fund	P3401-N

Keywords

cylindrical algebraic decomposition
quantifier elimination
equational constraints
satisfiability modulo theories
Non-linear real arithmetic

Access to Document

10.1007/s11786-025-00606-4

DEMU-ThirdRevisionAccepted author manuscript, 348 KB
s11786-025-00606-4Final published version, 480 KBLicence: CC BY

Cite this

@article{6da1703dbddc48d1961a4f70c32a8b5a,

title = "Iterated Resultants and Rational Functions in Real Quantifier Elimination",

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 \& 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 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.",

keywords = "cylindrical algebraic decomposition, quantifier elimination, equational constraints, satisfiability modulo theories, Non-linear real arithmetic",

author = "Davenport, \{James H.\} and Matthew England and Scott McCallum and Ali Uncu",

note = "{\textcopyright} The Author(s) 2025. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article{\textquoteright}s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article{\textquoteright}s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. CC BY",

year = "2025",

month = nov,

day = "19",

doi = "10.1007/s11786-025-00606-4",

language = "English",

volume = "19",

journal = "Mathematics in Computer Science",

issn = "1661-8270",

publisher = "Birkhauser",

}

TY - JOUR

T1 - Iterated Resultants and Rational Functions in Real Quantifier Elimination

AU - Davenport, James H.

AU - England, Matthew

AU - McCallum, Scott

AU - Uncu, Ali

N1 - © The Author(s) 2025. This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. CC BY

PY - 2025/11/19

Y1 - 2025/11/19

N2 - 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 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.

AB - 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 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.

KW - cylindrical algebraic decomposition

KW - quantifier elimination

KW - equational constraints

KW - satisfiability modulo theories

KW - Non-linear real arithmetic

U2 - 10.1007/s11786-025-00606-4

DO - 10.1007/s11786-025-00606-4

M3 - Article

SN - 1661-8270

VL - 19

JO - Mathematics in Computer Science

JF - Mathematics in Computer Science

M1 - 12

ER -

Iterated Resultants and Rational Functions in Real Quantifier Elimination

Abstract

Bibliographical note

Funding

Keywords

Access to Document

Fingerprint

Cite this