# Iterated Resultants and Rational Functions in
Real Quantifier Elimination

James H. Davenport  University of Bath
Bath, BA2 7AY
United Kingdom<EMAIL_ADDRESS>Matthew England  Coventry University,
Coventry, CV1 5FB
United Kingdom<EMAIL_ADDRESS>Scott McCallum  Macquarie
University,
Sydney, NSW 2109
Australia<EMAIL_ADDRESS>Ali K. Uncu  University of Bath
Bath, BA2 7AY
United Kingdom<EMAIL_ADDRESS>Austrian Academy of Sciences
Johann Radon Institute for Computational and Applied Mathematics
Linz, 4040
Austria<EMAIL_ADDRESS>
###### 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 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.

###### keywords:

cylindrical algebraic decomposition, quantifier elimination, equational
constraints, satisfiability module theories, non-linear real arithmetic

##  1 Introduction

In this paper we will extend some work on Cylindrical Algebraic Decomposition
(CAD) and Quantifier Elimination for logical formulae with polynomial
constraints over the reals (Real QE). These extensions take the form of tying
up loose ends from three papers that (subsets of) the present authors were
involved in. Two of the three papers were published within the proceedings of
the SC-Square Workshop [14], [39] and the other was published earlier on a
related topic to the first [33]. All three extensions should be of interest to
the SC-Square community, in particular those working on SMT in non-linear real
arithmetic utilising elements of CAD theory, or on computer algebra for Real
QE.

###  1.1 Cylindrical algebraic decomposition

CAD is an algorithm (and associated mathematical object) that decomposes real
space relative to an input (usually a set of polynomial or a logical formulae
whose atoms are polynomial constraints). CAD algorithms usually work through a
process of projection (whereby additional projection polynomials are produced
iteratively eliminating variables in each stage according to a fixed variable
ordering) and lifting (where decompositions of $\mathbb{R}^{i}$ are
iteratively produced for increasing $i$ relative to those projection
polynomials in the first $i$ variables of the ordering).

During lifting, each cell in $\mathbb{R}^{i}$ is lifted to a collection
(_stack_) of cells in $\mathbb{R}^{i+1}$ by evaluating the polynomials in
$\mathbb{R}^{i+1}$ at the sample point in $\mathbb{R}^{i}$ and then using
univariate real root isolation. We are able to conclude the decomposition over
the sample as representative of the decomposition over the whole cell so long
as the polynomials were _delineable_ over the cell, which informally means
they have the same root structure over any point in the cell (the same number
of real roots in the same order). The reader is referred to the collection
[12] for full details.

Over the past decade the theory of CAD has been used and further developed for
use the context of SMT for non-linear real arithmetic, which is the special
case of QE where all variables are existentially quantified. CAD
implementations have been developed that work more efficiently when used in
this context [23]. Further, whole new algorithms have been developed which use
the CAD theory in new ways, e.g. NLSAT [21], NuCAD [6] and Cylindrical
Algebraic Coverings [3], [24]; developed in part due to the SC-Square
initiative [2]. We expect that most of what we develop in this paper for CAD
could be adapted for these other variants.

###  1.2 Plan and contributions

We define in Section 2 the notation and theory of resultants needed for the
discussions that follow. In Section 3 we outline how the use of iterated
resultants in CAD leads to factorisations and then in Section 4 we describe
how in the case of multiple equational constraints in the input we could make
savings through the use of multivariate resultants. These three sections
reproduce our SC-Square 2023 Workshop paper [14] with important additions to
give clarity to the suggested optimisation and the impact it would have,
illustrated by a new example and complexity analysis.

After this, in Section 5, we revisit [33] which described an alternative
approach to make such savings in the case of just two equational constraints.
We correct a typo from the original paper [33] and provide a missing proof,
laying the foundation for future work in this area.

The original motivation and a common application of CAD is Real QE (for how
CAD may be utilised for this we again refer to the collection [12]). The
theory of both CAD and Real QE is usually expressed in polynomials, however in
practice, we are often faced with problems defined using rational functions.
In [39] we proposed two ways that this could be addressed in the case of SMT
for non-linear real arithmetic, i.e. the case where formulae are fully
existentially quantified. In Section 6 we extend this to the more general case
of Real QE, i.e. for any quantifier structure. We start by noting by means of
an example how a the straightforward approach of imposing denominator non-
vanishing is not sufficient for universal quantifiers, and then describe a
better approach.

##  2 Resultants

###  2.1 Univariate resultants

The resultant of two polynomials is another polynomial formed of their
coefficients (i.e.eliminating that original variable) that is equal to zero if
and only if the two original polynomials have a common root. Resultants are a
widely used tool in symbolic computation, and also in satisfiability checking
over non-linear arithmetic. In particular, they are a key ingredient of CAD
which in its traditional projection and lifting form [13] requires many
iterated univariate resultant calculations.

###  2.2 Notation

As usual, we will use $\mathop{\rm res}\nolimits$ (or $\mathop{\rm
res}\nolimits_{z}$ when we need to make the variable explicit) to denote
resultant, and $\mathop{\rm disc}\nolimits$ (or $\mathop{\rm
disc}\nolimits_{z}$) to denote the discriminant, the main tools used in CAD
projection.

The univariate resultant is often defined constructively in relation to the
determinant of the Sylvester matrix of the two polynomials. However, for use
in CAD we implicitly work with a square-free basis (and often an irreducible
basis to avoid having to make retrospective changes when new polynomials are
added to the mix111One further advantage of an irreducible basis is described
under $C$ in §4.5.). Thus for use in CAD we ignore repeated or common factors
as in the following example.

######  Example.

Let $f=x^{2}-1$ and $g=x^{2}-2x+1$ which, since they have a common root, means
their resultant using the traditional definition is zero.

However, for CAD we interpret their resultant as $\mathop{\rm
res}\nolimits_{x}\left((x-1)(x+1),(x-1)^{2}\right)$ and then since we delete
common factors this becomes $\mathop{\rm
res}\nolimits_{x}\left((x+1),(x-1)\right)$, which evaluates to 2.

######  Remark 2.1.

When we use the notation $\mathop{\rm res}\nolimits$ or $\mathop{\rm
disc}\nolimits$ in this paper we will always assume that repeated and common
factors have been removed from the output.

###  2.3 Multivariate resultants

We are grateful to [35] for a clear exposition of the results in [20], which
we have borrowed.

######  Definition 2.2.

Given $r$ homogeneous polynomials $F_{1},\ldots,F_{r}$ in
$x_{1},\ldots,x_{n}$, with indeterminate coefficients comprising a set $A$, an
integral polynomial $T$ in these indeterminates (that is, $T\in\mathbb{Z}[A]$)
is called an _inertia form_ for $F_{1},{\ldots},F_{r}$ if
$x_{i}^{\tau}T\in(F_{1},{\ldots},F_{r})$, for suitable $i$ and $\tau$.

Van der Waerden [41, §82] observes that the inertia forms comprise an ideal
$I$ of $\mathbb{Z}[A]$, and he shows further that $I$ is a principal ideal of
this ring. It follows from these observations that we may take the ideal $I$
of inertia forms to be the resultant system for the given
$F_{1},{\ldots},F_{r}$ in the sense that for special values of the
coefficients from field $K$, the vanishing of all elements of the resultant
system is necessary and sufficient for there to exist a non-trivial solution
to the system $F_{1}=0,{\ldots},F_{r}=0$ in some extension of $K$.

Now consider the case in which we have $n$ homogeneous polynomials in the same
number $n$ of variables. Let $F_{1},{\ldots},F_{n}$ be $n$ generic homogeneous
polynomials in $x_{1},{\ldots},x_{n}$ of positive total degrees
$d_{1},{\ldots},d_{n}$. That is, every possible coefficient of each $F_{i}$ is
a distinct indeterminate, and the set of all such indeterminate coefficients
is denoted by $A$. Let $I$ denote the ideal of inertia forms for
$F_{1},{\ldots},F_{n}$. Proofs of the following two propositions may be found
in [36].

######  Proposition 2.3.

[35, Proposition 5] $I$ is a nonzero principal ideal of $\mathbb{Z}[A]$:
$I=(R)$, for some $R\neq 0$. $R$ is uniquely determined up to sign. We call
$R$ the (generic multipolynomial) resultant of $F_{1},{\ldots},F_{n}$.

######  Proposition 2.4.

[35, Proposition 6] The vanishing of $R$ for particular $F_{1},{\ldots},F_{n}$
with coefficients in a field $K$ is necessary and sufficient for the existence
of a non-trivial zero of the system $F_{1}=0,{\ldots},F_{n}=0$ in some
extension of $K$.

The above considerations also lead us to the notion of a multivariate
resultant of $n$ non-homogeneous polynomials in $n-1$ variables. Consider a
given non-homogeneous $f(x_{1},{\ldots},x_{n-1})$ over field $K$ of total
degree $d$. We may write $f=H_{d}+H_{d-1}+\cdots+H_{0}$, where the $H_{j}$ are
homogeneous of degree $j$. Then $H_{d}$ is known as the leading form of $f$.
Recall that the homogenization $F(x_{1},{\ldots},x_{n})$ of $f$ is defined by
$F=H_{d}+H_{d-1}x_{n}+\cdots+H_{0}x_{n}^{d_{n}}$. Let $f_{1},{\ldots},f_{n}$
be particular non-homogeneous polynomials in $x_{1},{\ldots},x_{n-1}$ over $K$
of positive total degrees $d_{i}$, and with leading forms $H_{i,d_{i}}$. We
set $\mathop{\rm res}\nolimits(f_{1},{\ldots},f_{n})=\mathop{\rm
res}\nolimits(F_{1},{\ldots},F_{n})$ , where $F_{i}$ is the homogenization of
$f_{i}$. Then we have the following (see proof in [36]).

######  Proposition 2.5.

[35, Proposition 7] The vanishing of $\mathop{\rm
res}\nolimits(f_{1},{\ldots},f_{n})$ is necessary and sufficient for

either

the forms $H_{i,d_{i}}$ to have a common nontrivial zero over an extension of
$K$,

or

the polynomials $f_{i}$ to have a common zero over an extension of $K$.

Observe that the common zeros of the $f_{i}$ correspond to the affine
solutions of the system, whereas the non-trivial common zeros of the leading
forms correspond to the projective solutions on the hyperplane at infinity.

##  3 Factorisation of Iterated Univariate Resultants

Collins suggests in [13, pp. 177–178] that iterated resultants, where there
are “common ancestors” tend to factor. This was apparently responded to by van
der Waerden in a letter [43], which alas we have not seen, but the letter’s
contents are taken up again in [30], and there have been further developments
in [11, 25]. The work in [30] is based on the theory in [41], which [20] notes
has been deleted from more recent editions (such as [42]). The work in [11] is
based on that of [20].

Despite this factorisation being observed since the inception of CAD, we are
not aware of any optimisations in CAD implementations in regards to it.

###  3.1 Example

Consider these polynomials:

$\displaystyle f$ $\displaystyle=y^{2}+z^{2}+x+z-1,$ $\displaystyle g$
$\displaystyle=-x^{2}+y^{2}+z^{2}-1,$ $\displaystyle h$
$\displaystyle=x^{2}+y+z.$

Under variable ordering $z\succ y\succ x$ we may calculate the iterated
resultant:

$\begin{array}[]{rcl}\mathop{\rm res}\nolimits_{y}(\mathop{\rm
res}\nolimits_{z}(f,g),\mathop{\rm
res}\nolimits_{z}(f,h))&=&5x^{8}+16x^{7}+14x^{6}-2x^{5}-12x^{4}-8x^{3}+3x^{2}+2x\\\
&=&\underbrace{x\left(5x^{3}+6x^{2}-3x-2\right)}_{\hbox{spurious}}\underbrace{\left(x^{2}+x+1\right)\left(x^{2}+x-1\right)}_{\hbox{genuine}}\end{array}.$
(3.1)

We define the meaning of the labels below. An alternative computational path
may have calculated similarly

$\begin{array}[]{rcl}\mathop{\rm res}\nolimits_{y}(\mathop{\rm
res}\nolimits_{z}(f,g),\mathop{\rm
res}\nolimits_{z}(g,h))&=&5x^{8}+16x^{7}+18x^{6}+8x^{5}-5x^{4}-8x^{3}-2x^{2}+1\\\
&=&\underbrace{\left(x^{2}+x+1\right)\left(x^{2}+x-1\right)}_{\hbox{genuine}}\underbrace{\left(5x^{4}+6x^{3}+x^{2}-1\right)}_{\hbox{spurious}}.\end{array}$
(3.2)

The final choice would have been to calculate,

$\begin{array}[]{rcl}\mathop{\rm res}\nolimits_{y}(\mathop{\rm
res}\nolimits_{z}(f,h),\mathop{\rm
res}\nolimits_{z}(g,h))&=&2x^{4}+4x^{3}+2x^{2}-2\\\
&=&2\underbrace{\left(x^{2}+x+1\right)\left(x^{2}+x-1\right)}_{\hbox{genuine}}.\end{array}$
(3.3)

Up to constants (3.3) divides (3.2) and (3.1), but this need not happen in
general. What does happen in general is that, if we consider a Gröbner Basis,

$\verb+Basis+_{\tt
plex}(f,g,h)=\left\\{\left(x^{2}+x+1\right)\left(x^{2}+x-1\right),y-x,x^{2}+x+z\right\\},$
(3.4)

then we see that the basis polynomial in $x$ only divides all three iterated
resultants and in fact _is_ $\mathop{\rm res}\nolimits(f,g,h)$ in the sense of
Section 2.3. In this example, it is also (3.3), but again this need not happen
in general.

The labels above are made in regards to the roots of the tagged resultant
factors. The roots of the part we have labelled as “genuine” are

$\\{x:\exists y\exists zf(x,y,z)=g(x,y,z)=h(x,y,z)=0\\},$ (3.5)

whereas the roots of the part we have labelled as “spurious” are

$\left\\{x:\exists y\left(\exists z_{1}f(x,y,z_{1})=g(x,y,z_{1})=0\land\exists
z_{2}\neq z_{1}f(x,y,z_{2})=h(x,y,z_{2})=0\right)\right\\}.$ (3.6)

They are “spurious” in the sense that they do not go on to form true triple
roots. Nevertheless, they are $x$ values above which the topology changes, so
they cannot always be discarded. Note that Section 2.3 implies that there is
always a neat factorisation (over $\mathbb{Z}$ if that was the original ring)
into “genuine” versus “spurious”.

###  3.2 Effect of the variable ordering on the example

What happens if we take the variables in a different order? In ordering
$x\succ y\succ z$ we have:

$\mathop{\rm res}\nolimits_{y}(\mathop{\rm res}\nolimits_{x}(f,g),\mathop{\rm
res}\nolimits_{x}(f,h))=(z^{2}-1)^{2},$ (3.7) $\mathop{\rm
res}\nolimits_{y}(\mathop{\rm res}\nolimits_{x}(f,g),\mathop{\rm
res}\nolimits_{x}(g,h))=(z^{2}-1)^{4},$ (3.8) $\mathop{\rm
res}\nolimits_{y}(\mathop{\rm res}\nolimits_{x}(h,g),\mathop{\rm
res}\nolimits_{x}(f,h))=(z^{2}-1)^{4},$ (3.9)

and

$\verb+Basis+_{\tt
plex(x,y,z)}(f,g,h)=\left\\{z^{2}-1,y^{2}+y+z,x-y\right\\}.$ (3.10)

I.e. no spurious roots were uncovered with this ordering. The question of CAD
variable ordering is well studied and known to greatly effect the complexity
of CAD both in practice [17] and theory [8]. The introduction of spurious
factors in some orderings but not others may be a significant contributing
factor to this.

##  4 Discarding Spurious Factors in CAD

###  4.1 Equational constraints

One situation where the spurious factors can be concluded redundant is the
case of CAD with equational constraints.

######  Definition 4.1.

An _equational constraint_ is an equation whose truth is logically implied by
the input formula under study (either explicitly, appearing as a conjunction
to the rest of the formula, or otherwise implicitly).

Intuitively, the presence of an equational constraint reduces the dimension of
the possible solution set by one, and so we may hope to reduce some of the
computation in finding that solution set accordingly. There has been work to
this effect for CAD: starting with [31] and summarised in [19]. In particular,
we utilise later [32] which defined a reduced CAD projection operator
$P^{*}_{\mathcal{E}}(\mathcal{A})$ for calculating the CAD projection of a
polynomial set $\mathcal{A}$ in the presence of an equational constraint whose
factors are in $\mathcal{E}\subset\mathcal{A}$.

Consider the case of $k$ (explicit) equational constraints, along with some
additional constraints, all expressed in variables $x_{1},\dots,x_{n}$:

$\Phi\equiv f_{1}=0\land f_{2}=0\land\cdots
f_{k}=0\land\overline{\Phi}(f_{k+1},\ldots,f_{m}).$ (4.1)

The theory developed in [32] allows us to project with $\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{i})$, $i>1$, and $\mathop{\rm
disc}\nolimits_{x_{n}}(f_{i})$, $i\geq 1$, (as well as various coefficients,
which do not contribute to the degree explosion). In particular, we do not
need any $\mathop{\rm res}\nolimits(f_{i},f_{j})$ for $1<i<j$ which would be
included in a CAD projection without knowledge of equational constraints. Note
that here $f_{1}$ was selected as the _designated pivot_ equational constraint
for the projection (but any other equational constraint would have been valid
to designate as pivot).

After the first projection we cannot use any $f_{i}$ as an equational
constraint for the next projection, however, we can still make savings through
the presence of implicit equational constraints. E.g., since $f_{1}=0$ and
$f_{2}=0$, we know that $\mathop{\rm res}\nolimits_{x_{n}}(f_{1},f_{2})=0$
also. In fact, all the $\mathop{\rm res}\nolimits_{x_{n}}(f_{1},f_{i})$ are
equational constraints. Thus for the next projection we may take,

$\mathop{\rm res}\nolimits_{x_{n-1}}(\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2}),\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{i})),i>2,$ (4.2)

$\mathop{\rm res}\nolimits_{x_{n-1}}(\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2}),\mathop{\rm
disc}\nolimits_{x_{n}}(f_{i}))$, $i\geq 1$, and numerous discriminants.

###  4.2 Projection complexity with equational constraints

Traditional CAD projection to produce a sign-invariant decomposition for a set
of polynomials was shown to produce doubly exponentially many polynomials who
each have doubly exponential degree (in both cases taken with respect to the
number of projections). The projection operator from [32] reduces this by
taking advantage of equational constraints (producing a decomposition truth
invariant for the logical formula). See [19] for a full complexity analysis of
the various savings available from equational constraints to date. To
summarise, the we can extract savings sufficient to reduce the double exponent
in the number of polynomials, but not their degree.

We reproduce some of this analysis to demonstrate the issue we try to address
in the next subsection. We will observe the growth in projection polynomials,
focussing on resultants and discriminants (ignoring coefficients) and it is
these which exhibit degree growth.

Consider (4.1) and assume each $f_{i}$ is of degree at most $d$ (degree taken
in each variable separately). Hence we start with $m$ polynomials of degree
$d$. Using the projection operator from [32], after the first elimination, we
have

$\underbrace{\mathop{\rm res}\nolimits_{x_{n}}(f_{1},f_{2}),\ldots\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{m})}_{(m-1)\times\hbox{ degree
}2d^{2}},\underbrace{\mathop{\rm
disc}\nolimits_{x_{n}}(f_{1}),\ldots\mathop{\rm
disc}\nolimits_{x_{n}}(f_{m})}_{m\times\hbox{ degree }2d(d-1)}.$ (4.3)

For the sake of simplicity, regard these as $2m-1$ polynomials $g_{i}$ of
degree at most $2d^{2}$. Selecting $g_{1}=\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2})$ as the next designated pivot equational
constraint, we have the following after the second elimination:

$\underbrace{\mathop{\rm
res}\nolimits_{x_{n-1}}(g_{1},g_{2}),\ldots\mathop{\rm
res}\nolimits_{x_{n-1}}(g_{1},g_{2m-1})}_{(2m-2)\times\hbox{ degree
}8d^{4}},\underbrace{\mathop{\rm
disc}\nolimits_{x_{n-1}}(g_{1}),\ldots\mathop{\rm
disc}\nolimits_{x_{n-1}}(g_{2m-1})}_{(2m-1)\times\hbox{ degree
}8(d^{4}-d^{2})}.$ (4.4)

For the sake of simplicity, regard these as $4m-3$ polynomials $h_{i}$ of
degree at most $8d^{4}$. If we follow [32] then we must select one $h_{i}$ as
designated pivot equational constraint for the third elimination, say
$h_{1}=\mathop{\rm res}\nolimits_{x_{n-1}}(g_{1},g_{2})=\mathop{\rm
res}\nolimits_{x_{n-1}}(\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2}),\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{3}))$, and obtain:

$\underbrace{\mathop{\rm
res}\nolimits_{x_{n-2}}(h_{1},h_{2}),\ldots\mathop{\rm
res}\nolimits_{x_{n-2}}(h_{1},h_{4m-3})}_{(4m-4)\times\hbox{ degree
}128d^{8}},\underbrace{\mathop{\rm
disc}\nolimits_{x_{n-2}}(h_{1}),\ldots\mathop{\rm
disc}\nolimits_{x_{n-2}}(h_{4m-3})}_{(4m-3)\times\hbox{ degree
}128(d^{8}-d^{4})}.$ (4.5)

The equivalent of (4.2) after $k$ eliminations (i.e. eliminating all
equational constraints) has degree ${\mathcal{O}}\big{(}(2d)d^{2^{k}}\big{)}$
(i.e. doubly exponential).

###  4.3 Suggested use of multivariate resultants

In the setting of (4.1), we are really only interested in the genuine zeros of
the equational constraints, since away from these the formula will be
uniformly false and thus further refinement is unnecessary. Thus,

$A:=\mathop{\rm res}\nolimits_{x_{n-1}}(\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2}),\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{i}))$ (12) in [14]

is overkill, as it includes the “spurious” roots defined as in Equation (3.6),
as well as the genuine simultaneous roots of all three polynomials. (We
suggest for simplicity that the reader take $i=3$ in the equation immediately
above, although any specific $f_{i}$ with $i>2$ is permissible.) In the
earlier workshop version of this paper [14] we wrote:

> “So we can replace (12) by $B:=\mathop{\rm
> res}\nolimits(f_{1},f_{2},f_{i})$.”

This was careless wording. First, we should have again been clear that $i>2$
(and again we suggest taking $i=3$ for simplicity) and second we should have
been clear that we intended this multivariate resultant to be taken to
eliminate the last two variables $x_{n-1}$ and $x_{n}$. But most importantly,
we should have been clear that we intend to leave all the factors of $A$
within the set of projection polynomials found after the second elimination,
i.e. $\mathcal{J}_{n-2}$ using the notation from [32]. The replacement we
referred to was in the calculation of the third elimination where we suggest
to use $B$ instead of $A$ as the designated pivot equational constraint. More
specifically, we will take the irreducible factors of $B$ (which are
themselves amongst the irreducible factors of $A$) to form $\mathcal{E}_{n-2}$
in the computation of $P^{*}_{\mathcal{E}_{n-2}}(\mathcal{J}_{n-2})$.

We emphasise that we are not changing the set of projection factors, just
which factors are used to form the designated pivot equational constraint. The
correctness of this approach largely rests on the simple fact that $B$ is
itself an equational constraint of the input, albeit an implicit one, opening
the door to the use of the existing theory of [32].

A careful reader may notice that the theoretical framework of [32] is not
quite adequate for designating $B$ as a pivot equational constraint at level
$n-2$. The reason is that [32] implicitly assumes that any candidate pivot
constraint $e_{k}$ at level $k$ ($1<k<n$) is a product of elements of
$\mathcal{J}_{k}$, the set of projection polynomials at level $k$. (This was
to ensure $\mathcal{E}_{k}\subseteq\mathcal{J}_{k}$, and hence that the
subsequent semi-restricted projection is genuinely contained in the
unrestricted one.) However, the multivariate resultant $B$ need not be a
product of elements of $\mathcal{J}_{n-2}$.

Fortunately, we may easily propose a remedy. We designate $e_{n-2}=B$ and
$\mathcal{E}_{n-2}=\\{e_{n-2}\\}$, and observe
$\mathcal{F}_{n-2}\subseteq\mathcal{B}_{n-2}$, where $\mathcal{F}_{n-2}$ and
$\mathcal{B}_{n-2}$ are finest squarefree bases for $\mathcal{E}_{n-2}$ and
$\mathcal{J}_{n-2}$, respectively (by [30]). This ensures that the subsequent
semi-restricted projection is genuinely contained in the unrestricted one.

######  Remark 4.2.

The theory of [30, 32] is cast in terms of irreducible bases, partly for
simplicity and partly to align with the well-established practice (used in
QEPCAD, for example) of computing an irreducible basis at each level,
following projection, on efficiency grounds. Hence to use this theory, we also
need to speak in terms of irreducible bases, as in the previous paragraph. In
terms of implementation, we can use any square-free basis, because we have
justified that its irreducible factors are precisely what we need.

Since factorisation is generally good for efficiency (compare computing
$\mathop{\rm res}\nolimits(f_{1}f_{2},g)$ with separately computing
$\mathop{\rm res}\nolimits(f_{1},g)$ and $\mathop{\rm
res}\nolimits(f_{2},g)$), we can see that the primitive really needed is
“half-hearted factorisation”: do a square-free decomposition, and as much more
as you can easily do, which would probably mean giving up at the recombination
stage if the $p$-adic factors didn’t correspond to true factors over the
integers.

The theory of [32] moreover requires that $B$ is order invariant but this will
not require any changes to the projection process: the discriminant of $B$
will be produced already as it is a factor of the discriminant of $A$, and
similarly for the required coefficient of the projection factors. With $B$ the
designated pivot equational constraint we may query whether we need to add the
resultant of $B$ with $A$: but note that the intersection of $B$ with those
other factors of $A$ will already be produced as part of the discriminant of
$A$ and so this would obtain no additional projection factors.

Thus, our suggestion is valid using the theory of [32] and does not produce
any additional projection factors. However, as we will see next, we should get
savings by designated this smaller $B$ as equational constraint instead of
$A$.

###  4.4 Worked example

Consider the polynomials

$\begin{array}[]{rcl}f_{1}&:=&\left(z-y\right)^{3}+\left(x-w\right)^{3}-\left(x-1\right)y+zw,\\\
f_{2}&:=&x^{3}+y^{3}+z\left(y-1\right)+wx,\\\ f_{3}&:=&w^{3}+z^{3}+wy+zx,\\\
f_{4}&:=&\left(z+x\right)^{3}+\left(w+y\right)^{3}-zx+wy,\end{array}$

where at least $f_{1}$, $f_{2}$ and $f_{3}$ are equational constraints. We use
$D$ for the total degree of a polynomial.

  1. 1.

Select $f_{1}$ as the designated pivot equational constraint, and project out
$w$ following [32]. The polynomials are then $\mathop{\rm
res}\nolimits_{w}(f_{1},f_{i})$ and $\mathop{\rm disc}\nolimits_{w}(f_{i})$.
Call these polynomials $g_{1},\ldots,g_{7}$.

  2. 2.

As $f_{1},f_{2}$ are equational constraints, so is $g_{1}=\mathop{\rm
res}\nolimits_{w}(f_{1},f_{2})=\underbrace{-x^{9}-3x^{6}y^{3}-3x^{3}y^{6}-\cdots}_{\hbox{40
terms, $D=9$}}$. We can select this as the designated pivot equational
constraint and project out $z$, again following [32]. The polynomials are then
$\mathop{\rm res}\nolimits_{z}(g_{1},g_{i})$ and $\mathop{\rm
disc}\nolimits_{z}(g_{i})$. Call these polynomials $h_{1},\ldots,h_{13}$.

  3. 3.

$h_{1}=\mathop{\rm res}\nolimits_{z}(g_{1},g_{2})=\mathop{\rm
res}\nolimits_{z}(\mathop{\rm res}\nolimits_{w}(f_{1},f_{2}),\mathop{\rm
res}\nolimits_{w}(f_{1},f_{3}))$ is also an equational constraint. This is
$\underbrace{-512x^{81}-13824x^{78}y^{3}+\cdots}_{\hbox{3186 terms, $D=81$}}$.

Since $f_{1},f_{2},f_{3}$ are all equational constraints, we could select
$h_{1}$ as the designated pivot equational constraint, which is equivalent to
$A$ in (12) in [14].

However, following the suggestion we can instead use the multivariate
resultant

$\widehat{h}_{1}=\mathop{\rm
res}\nolimits_{w,z}(f_{1},f_{2},f_{3})=\underbrace{8x^{27}+72x^{24}y^{3}+288x^{21}y^{6}+\cdots}_{\hbox{359
terms, $D=27$}}$

as the designated pivot equational constraint.

  4. 4.

$h_{2}=\mathop{\rm res}\nolimits_{z}(g_{1},g_{3})=\mathop{\rm
res}\nolimits_{z}(\mathop{\rm res}\nolimits_{w}(f_{1},f_{2}),\mathop{\rm
res}\nolimits_{w}(f_{1},f_{4}))$ is the way $f_{4}$ appears when it comes to
projecting out $y$. In fact
$h_{2}=\underbrace{512x^{81}+13824x^{78}y^{3}+\cdots}_{\hbox{3214 terms,
$D=81$}}$. The options are

$\begin{array}[]{rcl}\mathop{\rm
res}\nolimits_{y}(h_{1},h_{2})&=&\underbrace{-4.97\cdot
10^{1265}x^{3894}+\cdots}_{\hbox{3651 terms, $D=3894$}},\\\ \mathop{\rm
res}\nolimits_{y}(\widehat{h}_{1},h_{2})&=&\underbrace{-2.6\cdot
10^{428}x^{1292}+\cdots}_{\hbox{1211 terms, $D=1292$}},\end{array}$

which already shows substantial advantages. If the $f_{i}$ were denser, the
savings in the number of terms would be greater still.

  5. 5.

In contrast to both the above,

$\begin{array}[]{rcl}\mathop{\rm
res}\nolimits_{w,z,y}(f_{1},f_{2},f_{3},f_{4})&=&\underbrace{-2.56\cdot
10^{35}x^{70}+\cdots}_{\hbox{62 terms, $D=70$}},\\\ \end{array}$

may be used if $f_{4}$ were an equation constraint and we were doing further
projections.

###  4.5 Why keep the iterated resultant in the projection set?

Why does $A$ have to stay in the projection set, $P^{*}_{\mathop{\rm
res}\nolimits_{x_{n}}(f_{1},f_{2})}(P_{f_{1}}^{*}(F))$, rather than being
replaced by $B$ there also? Write $A=BCD$, where $D$ is the product of those
factors of $A$ relatively prime to $B$, and $C=A/BD$, i.e. the product of
factors of $B$ which exist to higher multiplicity in $A$ than in $B$. So the
question is: “Why can we not ignore $C$ and $D$?”

$\bm{C}$

Let $b$ be a factor of a square-free decomposition of $B$. Then $B$ will be
order-invariant on the zeros of $b$. However, $A$ might not be, if $B$ factors
further as $b_{1}b_{2}$, and these divide $A$ to different multiplicities.
This problem is easy to solve, and indeed goes away if we take an irreducible
basis rather than just a square-free basis.

$\bm{D}$

The roots of $D$ should correspond to the “spurious” roots, and thus $f_{1}$,
$f_{2}$ and $f_{i}$ do not actually intersect here. This is true, but the
assertions in [32] are not about the triple intersections, even though these
are all we care about, so we would have to adjust the theory developed in [32]
and reprove validity. A further potential problem is that, although $D$ and
$B$ are relatively prime, their varieties might still intersect, giving rise
to a change in order of $A$, but not of $B$; a potential barrier to proving
such validity given that the correctness of [32] is based on a theory of
order-invariance.

In the case of only two equational constraints, a suitable change to the
statements from [32] to let us lift directly to a variety defined by two
constraints is given in [33]. We will revisit that in Section 5.

###  4.6 Impact on degree growth

Does the suggestion of Section 4.3 reduce the degree growth complexity
outlines in Section 4.2?. We saw there that the iterated resultants after $k$
eliminations have degree ${\mathcal{O}}\big{(}(2d)d^{2^{k}}\big{)}$. In
comparison, the theoretical multivariate resultant $\mathop{\rm
res}\nolimits(f_{1},\ldots,f_{k})$ has degree
${\mathcal{O}}\left(d^{k}\right)$ (the Bézout bound). More precisely, the
Dixon multivariate resultant is known to have degree $k!d^{k}$ (see [22, §4]).

Suppose we instead selected the multivariate resultant $h:=\mathop{\rm
res}\nolimits_{x_{n},x_{n-1}}(f_{1},f_{2},f_{3})$ as designated pivot
equational constraint for the third elimination. Then instead of (4.5) we get

$\underbrace{\mathop{\rm res}\nolimits_{x_{n-2}}(h,h_{2}),\ldots\mathop{\rm
res}\nolimits_{x_{n-2}}(h,h_{4m-3})}_{(4m-4)\times\hbox{ degree
}96d^{7}},\underbrace{\mathop{\rm
disc}\nolimits_{x_{n-2}}(h_{1}),\ldots\mathop{\rm
disc}\nolimits_{x_{n-2}}(h_{4m-3})}_{(4m-3)\times\hbox{ degree
}128(d^{8}-d^{4})}.$ (4.6)

Note that while as discussed in Section (4.3), we take the discriminant of the
larger $h_{1}$ rather than that of the smaller $h$.

At this stage, the saving does not seem great: $96d^{7}$ instead of
$128d^{8}$. This is because no savings were available for the first and second
elimination, with only the third allowing a smaller designated pivot
equational constraint. However, from now on all projections (until $k$
assuming the $k$ equational constraints were independent) can make use of a
multivariate resultant. So for the fourth elimination we are comparing the use
of an equational constraint of degree ${\mathcal{O}}(d^{8})$ if we follow
[32], to a multivariate resultant of degree ${\mathcal{O}}(d^{4})$ in the form
of $\mathop{\rm
res}\nolimits_{x_{n},x_{n-1},x_{n-2}}(f_{1},f_{2},f_{3},f_{4})$ using this
methodology of Section 4.3 (not one of the ${\mathcal{O}}(d^{7})$ resultants
in (4.6)).

In summary, while [18] observed that the use of existing optimisations for $k$
equational constraints reduces the double exponent of $m$ (the number of
polynomial constraints) from $n$ to $n-k$; here we show that the suggestion in
Section 4.3 gives the same reduction in the double exponent of $d$ (the degree
of the constraints) _in regards to the nested resultants_. However, the
overall degree growth is not controlled due to the discriminants in use. In
Section 5 we consider one alternative that might be pursued in the future to
counter this.

###  4.7 Detecting spurious factors

In the examples above the factors were marked as “spurious” or “genuine” via
manual analysis to see if the roots of the factors led to common zeros or not.
Are there alternatives to such manual detection?

We note that in some cases we can discard factors with based on their degree,
when this breaches the Bézout bound on the true multivariate resultant. I.e.,
if $\mathop{\rm res}\nolimits_{y}(\mathop{\rm
res}\nolimits_{z}(f,g),\mathop{\rm res}\nolimits_{z}(f,h))$ has an irreducible
factor of degree $>d^{3}$, it _must_ be spurious and can be discarded. Since
it is common for CAD implementation to factor polynomials, this is a cheap, if
incomplete, test.

######  Example.

For example, the following three 3-variable polynomials were created randomly
in Maple to have total degree 5:

$\displaystyle f$
$\displaystyle=-34x^{2}z^{3}-20y^{5}+7x^{2}y^{2}-43y^{3}z+63x+16z,$
$\displaystyle g$ $\displaystyle=13xz^{4}-27z^{4}-21xy^{2}+30yz-42x-81,$
$\displaystyle h$ $\displaystyle=-65xz^{4}+13z^{5}+30x^{3}z+17xy^{3}+25yz+78.$

Then $\mathop{\rm res}\nolimits_{y}(\mathop{\rm
res}\nolimits_{z}(f,g),\mathop{\rm res}\nolimits_{z}(f,h))$ factors into a
constant times two irreducible polynomials: one of degree $378$ and the other
of degree $89$. With no further computation we can identify the first as
spurious since its degree is greater than $5^{3}=125$. The second could be
genuine, or be another spurious factor: we may check manually that it is
indeed genuine.

In an example where we have multiple factors below the bound we could work
through them in turn keeping count of the sum of degrees of genuine factors as
we uncover then, in each case reducing the degree bound accordingly for any
further factors to be investigated as genuine.

###  4.8 Alternative projection operators

Though it would have to be proved, it seems very likely that the suggestions
and conclusions of this section, which were all developed in the McCallum
projection theory [29, 31, 32, 18], would apply also to equational constraints
within the Lazard projection theory [34, 16]. Here, equational constraints
introduce fresh challenges with “curtains” [37], similar to the challenges of
nullification in [27].

##  5 Delineability of Varieties for Equational Constraints

In Section 4, we suggested a fairly simple way to adapt CAD in the case of
multiple equational constraints to avoid some of the spurious roots. The
optimisation suggested, is easy to adapt existing implementations too and does
not require the development of new theory. However, the savings are limited as
outlined in Section 4.5, essentially to the projection phase rather than the
lifting phase.

An alternative approach was outlined in [33] by one of the present authors for
the case of two equational constraints. Here the authors define
$V\subset\mathbb{R}^{r}$ to be the real algebraic variety defined by the
conjunction of the two equational constraints: $f=0\land g=0$ whose defining
polynomials are in $x_{1},\dots x_{r}$. The paper defines a new notion of the
variety $V$ being delineable over a cell in $\mathbb{R}^{r-2}$, in contrast to
traditional CAD where delineability is defined for the polynomials. This
allows for the idea of projection and lifting between $\mathbb{R}^{r}$ and
$\mathbb{R}^{r-2}$ being single steps.

Along with defining this new delineability concept the paper presents two main
theorems. The first, Theorem 4.1, described conditions that allowed us to
conclude delineability of the variety over the cell. The second, Theorem 4.2,
aimed to describe conditions for other other polynomials present to be sign
invariant upon the cells of the variety. Together, these were to validate a
new projection operation to use in this case, making use of generalised
resultants and discriminants.

This offers a promising avenue for future development. In this paper we start
by providing some correction and clarification on those first ideas in [33].

###  5.1 Corrected version of Theorem 4.2

The theorems used the notation that $x$, $y$ and $z$ denote the $(r-2)$-tuple
$(x_{1},\ldots,x_{r-2})$, and the variables $x_{r-1}$, $x_{r}$, respectively.
The version of Theorem 4.2 published in [33] was as follows.

######  Theorem 5.1 ([33, Theorem 4.2]).

Let $f(x,y,z)$, $g(x,y,z)$ and $h(x,y,z)$ be real polynomials of positive
degrees with respect to $y$ and $z$. Let $R(x)$ be a generalised resultant of
$f$ and $g$ with respect to $y$ and $z$, and suppose $R(x)\neq 0$. Let $S$ be
a connected submanifold of $\mathbb{R}^{r-2}$ on which the variety $V$ of $f$
and $g$ is analytic delineable with respect to $y$ and $z$ and in which $R(x)$
is order-invariant. Suppose further that there is no common zero of the
polynomials $f$, $g$, $f_{z}$, $f_{y}$, $g_{z}$, $g_{y}$ in the cylinder
$S\times\mathbb{R}^{2}$ over $S$. Then $h$ is sign-invariant in each section
of $V$ over $S$.

The observant reader will notice that $h$ appears nowhere in the hypotheses,
other than the statement of its existence, which makes it unlikely that we are
able to draw conclusions about it. Indeed, the theorem required a simple
correction, which is made below in bold and red.

######  Theorem 5.2 ([33, Theorem 4.2 corrected]).

Let $f(x,y,z)$, $g(x,y,z)$ and $h(x,y,z)$ be real polynomials of positive
degrees with respect to $y$ and $z$. Let $R(x)$ be a generalised resultant of
$f$, $g$ and $\bm{h}$ with respect to $y$ and $z$, and suppose $R(x)\neq 0$.
Let $S$ be a connected submanifold of $\mathbb{R}^{r-2}$ on which the variety
$V$ of $f$ and $g$ is analytic delineable with respect to $y$ and $z$ and in
which $R(x)$ is order-invariant. Suppose further that there is no common zero
of the polynomials $f$, $g$, $f_{z}$, $f_{y}$, $g_{z}$, $g_{y}$ in the
cylinder $S\times\mathbb{R}^{2}$ over $S$. Then $h$ is sign-invariant in each
section of $V$ over $S$.

###  5.2 Proof of Theorem 4.2

The proof of Theorem 4.2 was omitted in [33] due to space constraints of the
publication. For the sake of completeness, we give here the proof of (the
corrected) Theorem 4.2.

###### Proof.

Let $\sigma$ be a section of $V$, determined by the continuous (indeed,
analytic) function $\theta:S\rightarrow\mathbb{R}^{2}$, where
$\theta(x)=(\theta_{y}(x),\theta_{z}(x))$ for all $x\in S$. By connectedness
of $\sigma$, it suffices to show that $h$ is sign-invariant in $\sigma$ near
an arbitrary point $(a,b,c)$ of $\sigma$. That $h$ is sign-invariant in
$\sigma$ near $(a,b,c)$ follows by continuity of $h$ in case $h(a,b,c)\neq 0$.
So henceforth assume $h(a,b,c)=0$. By one of the hypotheses, at least one of
$\partial f/\partial z$, $\partial f/\partial y$, $\partial g/\partial z$,
$\partial g/\partial y$ does not vanish at $(a,b,c)$. Without loss of
generality assume $\partial f/\partial z(a,b,c)\neq 0$ and $(a,b,c)=(0,0,0)$.

We aim to construct a function $R^{*}$, analytic near the origin in complex
$(r-2)$-space $\mathbb{C}^{r-2}$, whose zero set is the projection onto
$\mathbb{C}^{r-2}$ of the portion of the complex variety of $f$, $g$ and $h$
near the origin in $\mathbb{C}^{r}$. This will require several steps, the
first of which is as follows. Since $\partial f/\partial z(0,0,0)\neq 0$, we
may apply Hensel’s lemma (Theorem 3.1 of [30]) to $f$ near the origin in
complex $(r-1)$-space $\mathbb{C}^{r-1}$. By this lemma we conclude there is a
polydisc $\Delta_{1}$ about the origin and polynomials in $z$,
$f_{1}(x,y,z)=z-\xi(x,y)$ and $f_{2}(x,y,z)$, whose coefficients are elements
of the formal power series ring $\mathbb{R}[[x,y]]$, absolutely convergent in
$\Delta_{1}$, such that $\xi(0,0)=0$, $f_{2}(0,0,0)\neq 0$, and
$f=f_{1}f_{2}$. Since a function defined as a sum of a convergent power series
is analytic, $\xi(x,y)$ and the coefficients of $f_{2}$ are analytic in
$\Delta_{1}$.

The reader might guess that we could quickly complete the construction of the
desired function $R^{*}$ by setting $R^{*}(x)$ to be a generalized resultant
of $f_{1}$, $g$ and $h$ with respect to $y$ and $z$. However, since $f_{1}$ is
not known to be polynomial in $y$ (though it is in $z$), such a proposed
definition is not valid. Consequently, a more involved process is needed.

For any $\delta>0$, we denote by $\Delta(0;\delta)$ the disc in $\mathbb{C}$
about the origin of radius $\delta$. The second step of our construction
process follows. Put $P(x,y)=\mathop{\rm
res}\nolimits_{z}(f_{1},g)=g(x,y,\xi(x,y))$, for all $(x,y)\in\Delta_{1}$.
Where $m>0$ denotes the intersection mutiplicity of $f(0,y,z)$ and $g(0,y,z)$
at $(0,0)$, we may infer that $y=0$ is a zero of $P(0,y)$ of multiplicity $m$
(by a slight extension of Theorem 5.3 of Chapter IV of [44], since the zeros
of $f$ are the same as the zeros of $f_{1}$ near the origin, and the plane
curves $f_{1}(0,y,z)=0$ and $g(0,y,z)=0$ have no intersections on the $z$-axis
except at $z=0$). Hence, by the $(r-1)$-variable analogue of the Weierstrass
preparation theorem (as presented in Lecture 16 of [1]), there is a polydisc
$\Delta_{2}=\Delta_{2}^{\prime}\times\Delta(0;\delta_{2})\subset\Delta_{1}$
about the origin in $\mathbb{C}^{r-1}$, a polynomial
$P_{1}(x,y)=y^{m}+a_{1}(x)y^{m-1}+\cdots+a_{m}(x)$, with the
$a_{i}(x)\in\mathbb{R}[[x]]$, absolutely convergent in $\Delta_{2}^{\prime}$,
and an element $P_{2}(x,y)$ of $\mathbb{R}[[x,y]]$, absolutely convergent in
$\Delta_{2}$, such that $P_{1}(0,y)=y^{m}$, $P_{2}(0,0)\neq 0$, and
$P=P_{1}P_{2}$.

To begin the third step of our construction, we put $T(x,y)=\mathop{\rm
res}\nolimits_{z}(f_{1},h)$. By the Weierstrass division theorem (Lecture 16
of [1]), there exists a polydisc
$\Delta_{3}=\Delta_{3}^{\prime}\times\Delta(0;\delta_{3})\subset\Delta_{2}$,
an element $Q(x,y)$ of $\mathbb{R}[[x,y]]$, absolutely convergent in
$\Delta_{3}$, and an element $T^{*}(x,y)$ of $\mathbb{R}[[x]][y]$, of degree
in $y$ at most $m-1$, whose coefficients are absolutely convergent in
$\Delta_{3}^{\prime}$, such that $T=P_{1}Q+T^{*}$. By the analyticity (hence
continuity) of the coefficients $a_{i}(x)$ of $P_{1}$, and polynomial root
system continuity (Theorem (1,4) of [26]), we may if needed refine
$\Delta_{3}^{\prime}$ to a smaller polydisc about the origin to ensure that
for every fixed $x\in\Delta_{3}^{\prime}$, each root of $P_{1}(x,y)$ is in
$\Delta(0;\delta_{3})$.

We may now complete our construction of $R^{*}$: we put $R^{*}(x)=\mathop{\rm
res}\nolimits_{y}(P_{1},T^{*})$. We claim that the zero set of $R^{*}$ is
contained in the zero set of $R$ in $\Delta_{3}^{\prime}$. The proof of this
claim is as follows. Let $\alpha$ be an element of $\Delta_{3}^{\prime}$ and
suppose that $R^{*}(\alpha)=0$. Then there exists $\beta\in\mathbb{C}$ such
that $P_{1}(\alpha,\beta)=T^{*}(\alpha,\beta)=0$. Since each root of
$P_{1}(\alpha,y)$ is in $\Delta(0;\delta_{3})$, we have
$\beta\in\Delta(0;\delta_{3})$. Hence we can legally substitute
$(\alpha,\beta)$ for $(x,y)$ in the power series identity $T=P_{1}Q+T^{*}$,
from which we deduce $T(\alpha,\beta)=0$. The same substitution in the power
series identity $P=P_{1}P_{2}$ yields $P(\alpha,\beta)=0$. Hence, with
$\gamma=\xi(\alpha,\beta)$, we have
$g(\alpha,\beta,\gamma)=h(\alpha,\beta,\gamma)=0$. Substitution of
$(\alpha,\beta,\gamma)$ into $f=f_{1}f_{2}$ yields $f(\alpha,\beta,\gamma)=0$.
Therefore, by Theorem 2.3 of [33] we have $R(\alpha)=0$. The claim is proved.

Next, by Theorem 5.1 of [10], there exists a polydisc
$\Delta_{4}^{\prime}\subset\Delta_{3}^{\prime}$, an analytic function
$R^{\prime}$ in $\Delta_{4}^{\prime}$, and an integer $n\geq 1$ such that
$R^{n}=R^{*}R^{\prime}$ in $\Delta_{4}^{\prime}$. Since $R$ and $R^{*}$ have
real power series representations, so does $R^{\prime}$ (because the imaginary
part of the power series expansion for $R^{\prime}$ about the origin must be
0). Therefore, $R^{\prime}$ is analytic in the box
$B_{4}^{\prime}=\Delta_{4}^{\prime}\cap\mathbb{R}^{r-2}$. By Lemma A.3 of
[28], since $R$ is order-invariant in $S$ by hypothesis, $R^{*}$ is order-
invariant in $S\cap B_{4}^{\prime}$. But $R^{*}(0)=0$, since $f_{1}$, $g$ and
$h$ all vanish at the origin. Hence $R^{*}(x)=0$, for all $x\in S\cap
B_{4}^{\prime}$.

We conclude our proof as follows. We claim that for every fixed $x\in S\cap
B_{4}^{\prime}$, $\theta_{y}(x)$ is a root of $P_{1}(x,y)$ of multiplicity
$m$, hence the unique root of $P_{1}(x,y)$. To prove this claim, take some
fixed $x\in S\cap B_{4}^{\prime}$. Now the intersection multiplicity of the
curves $f(x,y,z)=0$ and $g(x,y,z)=0$ at $(\theta_{y}(x),\theta_{z}(x))$ is $m$
since the intersection multiplicity of $f(0,y,z)$ and $g(0,y,z)$ at $(0,0)$ is
$m$ (previously stated) and $V$ is analytic delineable with respect to $y$ and
$z$ on $S$ (a key hypothesis). Therefore $y=\theta_{y}(x)$ is a root of
$P(x,y)$, hence of $P_{1}(x,y)$, of multiplicity at least $m$, by a slight
extension of Theorem 5.3 of Chapter IV of [44]. Since $\deg_{y}P_{1}=m$, the
root $y=\theta_{y}(x)$ of $P_{1}(x,y)$ has multiplicity exactly equal to $m$,
and hence this number is the unique root of $P_{1}(x,y)$. The claim is proved.

Our final claim is that $h(x,\theta_{y}(x),\theta_{z}(x))=0$, for all $x\in
S\cap B_{4}^{\prime}$. To prove this, take some fixed $x\in S\cap
B_{4}^{\prime}$. Then $R^{*}(x)=0$ (established in the previous paragraph).
Therefore, there exists $\beta\in\Delta(0;\delta_{3})$ such that
$P_{1}(x,\beta)=T^{*}(x,\beta)=0$. But $y=\theta_{y}(x)$ is the unique root of
$P_{1}(x,y)$ (already proved within this paragraph). Therefore
$\beta=\theta_{y}(x)$. We deduce $T(x,\theta_{y}(x))=0$ (by substituting
$(x,\theta_{y}(x))$ into the identity $T=P_{1}Q+T^{*}$). Hence
$h(x,\theta_{y}(x),\theta_{z}(x))=0$, by definition of $T$. Our final claim is
proved, and the proof of the theorem is now complete. ∎

##  6 Rational Functions as Input

The theory of CAD is cast in terms of polynomials, but in practice, problems
are often presented involving rational functions. How should we reconcile
this? The SMTLIB format [5] only allows polynomial constraints, and the same
is true of, for example, the Tarski system [40].

In the “New Perspectives in Symbolic Computation and Satisfiability Checking”
Dagstuhl 2022 meeting [4] allowing rational functions in the SMTLIB format and
letting SMT-solvers handle them were discussed openly, following the talk of
Duterte [4, §3.10] . The main two concerns raised against allowing rational
functions in SMTLIB language were “What would happen if a solver re-packages
and does arithmetic with an object of the form $x/0$?” and “What if the solver
splits the problem and, on a branch not directly related to the rational
function, finds an assignment that makes the rational function undefined?” It
was also made clear that defining objects of the form $x/0$, even when they
respect equalities (i.e. $x=z\Leftrightarrow x/0=z/0$), can be lead to proving
wrong results. These concerns demotivated the cohort to work on the problem,
let alone to come up with a unified solution.

In the context of real satisfiability problems, these questions were addressed
in an SC-Square 2022 Workshop paper by three of the present authors [39] who
introduced and compared two approaches, which we will recap shortly. Their
approach was to interpret and preprocess rational functions in a
mathematically consistent way to make the semantic concerns of the previous
paragraph extraneous. The formal manipulations suggested are easy to be
carried out by SMT-solvers and this way rational functions can be allowed in
SMT format as valid input. While valid for the fully existential context of
SMT, the discussion in [39] will be shown to be incomplete. We introduce the
problem and provide a proposed solution in this section for any quantification
structure.

###  6.1 The problem with supposing non-zero denominators

The material in this subsection was produced following an email we received
from Chris Brown [7] stimulated in turn by a conversation he had with Zoltan
Kovács: Zoltan wants to be able to send rational formulas to the Tarski
software from his GeoGebra Discovery software [9]. He suggested adding the
requirement of non-vanishing denominators but Chris noted the problems with
this by means of the following example.

Suppose the procedure is that, for a given atom $A$ which involves a non-
trivial denominator $D$, we consider instead $\bar{A}\land D\not=0$, where
$\bar{A}$ is some simplification of $A$ that is polynomial, e.g. multiplying
up by the denominator $D$. Let us follow this procedure, looking at the
problem

$\forall x\left[\frac{1}{x^{2}}\geq 0\right].$

So the procedure lead us to study

$\forall x\left[{x^{2}}\not=0\land{1}\geq 0\right].$

For $x=0$, the statement on the line above is false (from the first clause).
Consider next the negation of our original example: $\exists
x\,[1/{x^{2}}<0]$. The same procedure would lead us to study

$\exists x\left[x^{2}\not=0\land 1<0\right],$

which is also false (this time from the second clause). We cannot have a
statement and its negation both false, which implies that the procedure was
not a logical implication.

###  6.2 Restricted domains and conditional quantification

The procedure above does not take into account that the original rational
functions are defined on restricted domains. The problem $\forall
x[1/x^{2}\geq 0]$ needs to be addressed within the domain of $1/x^{2}$, where
all the points on which it is not defined (only $x=0$ in this case) should be
left behind. More generally, we should be studying the following restricted
quantification structure:

$\forall x,\underbrace{\text{for which }A\text{ is defined}}_{condition},A.$

However, most Quantifier Elimination procedures do not support such a
statement directly. The logical reduction of a conditional $\forall$ statement
is an implication, which turns this problem to

$\forall x\in\mathbb{R},A\text{ is defined}\Rightarrow{A}.$

Recall that logical implications make no assertion on what happens when the
hypothesis is false. I.e. one can replace the $``A\text{ is
defined}\Rightarrow"$ directly with the conditions on the domain.

###  6.3 Prior work on denominators

Rational functions and how to deal with the possible zeros of the denominators
in the context of SMT for non-linear real arithmetic calculations have been a
part of the SC-Square conversation, at least since the Dagstuhl 2022 meet [4].
This led to the inclusion of Section 3 of our 2022 paper [39] where we
discussed how the problem could be handled in at least two ways, and further
that the choice of approach led to different conclusions on the subsequent
best SMT solver.

Given polynomials $f(\vec{x},y),g(\vec{x},y)\in\mathbb{Z}[\vec{x},y]$, with
$f(\vec{x},y)/g(\vec{x},y)$ in minimal terms222i.e. there is no $(\vec{x},y)$
such that both $f(\vec{x},y)=0$ and $g(\vec{x},y)=0$ together., we suggested
two possible equivalences:

$\displaystyle\exists
y\left[\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right]$
$\displaystyle\Longleftrightarrow\exists y[g(\vec{x},y)\not=0\land
f(\vec{x},y)g(\vec{x},y)\,\sigma\,0],$ (6.1) $\displaystyle\exists
y\left[\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right]$
$\displaystyle\Longleftrightarrow\exists y[(g(\vec{x},y)>0\land
f(\vec{x},y)\,\sigma\,0)$ (6.2)
$\displaystyle\qquad\qquad\lor(g(\vec{x},y)<0\land 0\,\sigma\,f(\vec{x},y))],$

where in both cases $\sigma$ is a relation operator from
$\\{=,\not=,>,<,\leq,\geq\\}$.

We argue now that these simplifications proposed in [39] both take into
account the implied conditions on the domain and thus do not suffer from the
issues of the preceding sections.

Any problem involving only polynomials has the whole of $\mathbb{R}$ for each
variable as its domain. However, while handling rational functions, under the
hood, we have to deal with the domain of functions $f/g$. I.e., $\exists
y[{f(\vec{x},y)}/{g(\vec{x},y)}\,\sigma\,0]$ does not translate to $\exists
y\in\mathbb{R}[{f(\vec{x},y)}/{g(\vec{x},y)}\,\sigma\,0]$, but instead
translates to

$\exists
y\in\\{z:g(\vec{x},z)\not=0)\\}\left[\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right].$

However, this is exactly the same as

$\exists
y\left[g(\vec{x},y)\not=0\land\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right],$

and thus the simplifications from [39] are faithful to the domains of the
rational functions.

We did not run into the same problems as Section 6.1 because we considered
only existential quantification.

###  6.4 Universal quantification and denominators

Now consider a rational function constraint under universal quantification:

$\forall y\left[\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right].$

As outlined in Section 6.2 this should actually be read as

$\forall
y\in\\{z:g(\vec{x},z)\not=0)\\}\left[\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right]$

Then its logical equivalent with an unconditional quantification must use
implication to avoid making a statement when the denominator vanishes:

$\displaystyle\forall
y\left[g(\vec{x},y)\not=0\Rightarrow\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right],$
$\displaystyle\Longleftrightarrow\,$ $\displaystyle\forall
y\left[\lnot\left(g(\vec{x},y)\neq
0\right)\lor\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right],$
$\displaystyle\Longleftrightarrow\,$ $\displaystyle\forall
y\left[g(\vec{x},y)=0\lor\frac{f(\vec{x},y)}{g(\vec{x},y)}\,\sigma\,0\right].$

###  6.5 Solving the problem in Section 6.1

To finish this section let us readdress the example introduced in Section 6.1.
In the first step below we make explicit the restricted domain and in the
second we apply the universal quantification equivalent of (6.1), the first of
the two approaches to clearing the denominator from [39].

$\displaystyle\forall x\left[\frac{1}{x^{2}}\geq 0\right]$
$\displaystyle\Longleftrightarrow\forall
x\left[{x^{2}}\not=0\Rightarrow\frac{1}{x^{2}}\geq 0\right]$
$\displaystyle\Longleftrightarrow\forall x\left[\lnot({x^{2}}\not=0)\lor
x^{2}\geq 0\right]$ $\displaystyle\Longleftrightarrow\forall
x\left[{x^{2}}=0\lor x^{2}\geq 0\right].$

The final line can be clearly seen as true for every $x\in\mathbb{R}$. If we
consider the negation of the original example then we analyse this as in
Section 6.1 and find it false. This time the problem and its negation are not
the same.

If we had followed instead the universl equivalent of (6.2), we would get

$\displaystyle\forall x\left[\frac{1}{x^{2}}\geq 0\right]$
$\displaystyle\Longleftrightarrow\forall
x\left[{x^{2}}\not=0\Rightarrow\frac{1}{x^{2}}\geq 0\right]$
$\displaystyle\Longleftrightarrow\forall
x\left[\lnot({x^{2}}\not=0)\lor\left((x^{2}>0\land 1\geq 0)\lor(x^{2}<0\land
1\leq 0)\right)\right]$ $\displaystyle\Longleftrightarrow\forall
x\left[{x^{2}}=0\lor(x^{2}>0\land 1\geq 0)\right],$

which is also true for all $x\in\mathbb{R}$.

##  7 Future Work

###  7.1 Iterated resultants for CAD

The work in Section 4 looked only at the resultants, not the discriminants,
and indeed only at resultants of resultants. Undoubtedly something similar can
be said about, for example

$\mathop{\rm res}\nolimits_{y}(\mathop{\rm res}\nolimits_{z}(f,g),\mathop{\rm
disc}\nolimits_{z}(f)).$ (7.1)

We observe that, in the case of the polynomials from Section 4.7, the
evaluation of (7.1) is a perfect square, and this seems to be true in general.
We would need a complete solution for resultants of discriminants,
discriminants of resultants and discriminants of discriminants in order to
firmly conclude a reduction in the worse case degree growth.

Further, if we look again at (3.3) from the example in Section 3, we see that
this polynomial, which is the “genuine” part, factors further, and one factor
has no real roots. Hence this factor can be discarded, though there is not
much benefit, since we are at the univariate phase. Nevertheless, this shows
that even the “genuine” part may still be overkill for _real_ geometry. Can we

  1. a)

detect that a factor of a resultant etc. has no real components; and

  2. b)

use this to further reduce the polynomials? Furthermore,

  3. c)

can we make any meaningful statement about the complexity implications of
this?

An alternative route for future work would be to generalise the ideas in [33]
that we revisited in Section 5 beyond the case of two equational constraints.

###  7.2 Iterated resultants in CAD variants

Over the past decade the theory of CAD has been used within a variety of other
algorithms, e.g. NLSAT [21], NuCAD [6] and Cylindrical Algebraic Coverings
[3], [24]. These were developed for, or inspired by, the ideas in the
satisfiability checking community. It would be natural to ask whether the
optimisations described here for CAD would also apply for these other
algorithms.

With Cylindrical Algebraic Coverings [3], each polynomial has (at least one)
explicit reason for being where it is in the computation. For example,
$\mathop{\rm res}\nolimits_{x_{n}}(f_{1},f_{2})$ might be in the computation
because of a specific root $\alpha$, where it is the case for $x_{n-1}>\alpha$
(until the next point) the regions ruled out by $f_{1}$ and $f_{2}$ overlap,
whereas for $x_{n-1}<\alpha$ we need a further reason to rule out regions. The
same might be true of $\mathop{\rm res}\nolimits_{x_{n}}(f_{1},f_{3})$, needed
because of a specific root $\beta$. Then (4.2) tracks where $\alpha$ and
$\beta$ meet. Hence in this context we are interested only in genuine roots,
and again we can replace (4.2) by $\mathop{\rm
res}\nolimits(f_{1},f_{2},f_{i})$. Such ideas would need to be worked through
precisely with an implementation of the coverings algorithm.

### Acknowledgements

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 acknowledges the support of
Austrian Science Fund (FWF) project P3401-N.

The authors are grateful to Jasper Nalbach whose questions about [14] led us
to provide the clarification in Section 4.3 and the new Section 4.5; and to
Chris Brown and Zoltan Kovács whose conversation prompted Section 6. We are
also grateful to Gregory Sankaran, Tereso del Río and Amirhosein Sadeghi
Manesh for useful conversations on equational constraints.

## References

  * [1] S.S. Abhyankar.  Algebraic Geometry for Scientists and Engineers, volume 35 of Mathematical Surveys and Monographs.  American Mathematical Society, 1990.
  * [2] E. Ábrahám, B. Becker, A. Bigatti, B. Buchberger, A. Cimatti, J.H. Davenport, M. England, P. Fontaine, S. Forrest, D. Kroening, W. Seiler, and T. Sturm.  SC2: Satisfiability Checking meets Symbolic Computation (Project Paper).  In Proceedings CICM 2016, pages 28–43, 2016.  doi:10.1007/978-3-319-42547-4_3.
  * [3] E. Ábrahám, J.H. Davenport, M. England, and G. Kremer.  Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings.  Journal of Logical and Algebraic Methods in Programming, 119, 2021\.  doi:10.1016/j.jlamp.2020.100633.
  * [4] Erika Ábrahám, James H. Davenport, Matthew England, and Alberto Griggio.  New Perspectives in Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 22072).  Dagstuhl Reports, 12(2):67–86, 2022.  URL: https://drops.dagstuhl.de/opus/volltexte/2022/16931, doi:10.4230/DagRep.12.2.67.
  * [5] C. Barrett, P. Fontaine, and C. Tinelli.  The SMT-LIB Standard: Version 2.6.  http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, 2021\.
  * [6] C.W. Brown.  Open Non-uniform Cylindrical Algebraic Decompositions.  In Proceedings ISSAC 2015, pages 85–92, 2015.  doi:10.1145/2755996.2756654.
  * [7] C.W. Brown.  Why adding non-vanishing conditions on all denominators is problematic.  Communication to Davenport 13 October, 2023.
  * [8] C.W. Brown and J.H. Davenport.  The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition.  In C.W. Brown, editor, Proceedings ISSAC 2007, pages 54–60, 2007\.  doi:10.1145/1277548.1277557.
  * [9] C.W. Brown, Z. Kovács, and R. Vajda.  Supporting Proving and Discovering Geometric Inequalities in GeoGebra by using Tarski.  Automated Deduction in Geometry ADG 2021 EPTCS, 352:156–166, 2021\.  URL: https://arxiv.org/abs/2201.00544v1.
  * [10] C.W. Brown and S. McCallum.  On using bi-equational constraints in CAD construction.  In Proceedings ISSAC 2005, pages 76–83, 2005.  doi:10.1145/1073884.1073897.
  * [11] L. Busé and B. Mourrain.  Explicit Factors of some Iterated Resultants and Discriminants.  Math. Comp., 78:345–386, 2009.  doi:10.1090/S0025-5718-08-02111-X.
  * [12] B. Caviness and J. Johnson.  Quantifier Elimination and Cylindrical Algebraic Decomposition.  Texts & Monographs in Symbolic Computation. Springer-Verlag, 1998.  doi:10.1007/978-3-7091-9459-1.
  * [13] G.E. Collins.  Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition.  In H. Brakhage, editor, Proceedings 2nd. GI Conference Automata Theory & Formal Languages, volume 33 of Springer Lecture Notes in Computer Science, pages 134–183, 1975.  doi:10.1007/3-540-07407-4_17.
  * [14] James H. Davenport and Matthew England.  Iterated resultants in CAD.  In Erika Ábrahám and Thomas Sturm, editors, Proceedings of the 8th SC-Square Workshop, CEUR-WS Proceedings, volume 3455, pages 54–60, 2023\.  URL: http://ceur-ws.org/Vol-3455/.
  * [15] J.H. Davenport, M. England, A. Griggio, T. Sturm, and C. Tinelli, editors.  Symbolic Computation and Satisfiability Checking: special issue of Journal of Symbolic Computation, volume 100. Elsevier, 2020.
  * [16] J.H. Davenport, A.S. Nair, G.K. Sankaran, and A.K. Uncu.  Lazard-style CAD and Equational Constraints.  In G. Jeronimo, editor, Proceedings ISSAC 2023, pages 218–226, 2023\.  doi:10.1145/3597066.3597090.
  * [17] Tereso del Río and Matthew England.  New Heuristic to Choose a Cylindrical Algebraic Decomposition Variable Ordering Motivated by Complexity Analysis.  In François Boulier, Matthew England, Timur M. Sadykov, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing CASC 2022, volume 13366 of Lecture Notes in Computer Science, pages 300–317, 2022.  doi:10.1007/978-3-031-14788-3_17.
  * [18] M. England, R. Bradford, and J.H. Davenport.  Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition.  In D. Robertz, editor, Proceedings ISSAC 2015, pages 165–172, 2015\.  doi:10.1145/2755996.2756678.
  * [19] M. England, R.J. Bradford, and J.H. Davenport.  Cylindrical Algebraic Decomposition with Equational Constraints.  In Davenport et al. [15], pages 38–71.  doi:10.1016/j.jsc.2019.07.019.
  * [20] J.P. Jouanolou.  Le Formalisme du Résultant.  Advances in Mathematics, 90:117–263, 1991.  doi:10.1016/0001-8708(91)90031-2.
  * [21] D. Jovanović and L. de Moura.  Solving Non-Linear Arithmetic.  In Proceedings IJCAR 2012, pages 339–354, 2012.  doi:10.1007/978-3-642-31365-3_27.
  * [22] D. Kapur and T. Saxena.  Comparison of various multivariate resultant formulations.  In Proceedings ISSAC 1915, pages 187–194, 1995.  doi:https://doi.org/10.1145/220346.220370.
  * [23] G. Kremer and E. Ábrahám.  Fully Incremental CAD.  In Davenport et al. [15], pages 11–37.  doi:https://doi.org/10.1016/j.jsc.2019.07.018.
  * [24] Gereon Kremer and Jasper Nalbach.  Cylindrical algebraic coverings for quantifiers.  In Uncu and Barbosa [38], pages 1–9.  URL: https://ceur-ws.org/Vol-3458/.
  * [25] D. Lazard and S. McCallum.  Iterated Discriminants.  J. Symbolic Comp., 44:1176–1193, 2009.  doi:10.1016/j.jsc.2008.05.006.
  * [26] M. Marden.  Geometry of polynomials, 2nd edition.  American Mathematical Soc., 1966.
  * [27] S. McCallum.  An Improved Projection Operation for Cylindrical Algebraic Decomposition.  PhD thesis, University of Wisconsin-Madison Computer Science, 1984.
  * [28] S. McCallum.  An Improved Projection Operation for Cylindrical Algebraic Decomposition of Three-dimensional Space.  J. Symbolic Comp., 5:141–161, 1988.  doi:10.1016/S0747-7171(88)80013-0.
  * [29] S. McCallum.  An Improved Projection Operation for Cylindrical Algebraic Decomposition.  [12], pages 242–268.  doi:10.1016/S0747-7171(88)80010-5.
  * [30] S. McCallum.  Factors of Iterated Resultants and Discriminants.  J. Symbolic Comp., 27:367–385, 1999.  doi:doi:10.1006/jsco.1998.0257.
  * [31] S. McCallum.  On Projection in CAD-Based Quantifier Elimination with Equational Constraints.  In S. Dooley, editor, Proceedings ISSAC ’99, pages 145–149, 1999\.  doi:10.1145/309831.309892.
  * [32] S. McCallum.  On Propagation of Equational Constraints in CAD-Based Quantifier Elimination.  In B. Mourrain, editor, Proceedings ISSAC 2001, pages 223–230, 2001\.  doi:10.1145/384101.384132.
  * [33] S. McCallum and C.W. Brown.  On delineability of varieties in CAD-based quantifier elimination with two equational constraints.  In Proceedings ISSAC 2009, pages 71–78, 2009.  doi:10.1145/1576702.1576715.
  * [34] S. McCallum, A. Parusiński, and L. Paunescu.  Validity proof of Lazard’s method for CAD construction.  J. Symbolic Comp., 92:52–69, 2019.  doi:10.1016/j.jsc.2017.12.002.
  * [35] S. McCallum and F. Winkler.  Differential resultants.  ITM Web of Conferences Article 01005, 20, 2018.  doi:10.1051/itmconf/20182001005.
  * [36] S. McCallum and F. Winkler.  Resultants: Algebraic and Differential.  Technical Report RISC18-08, Johannes Kepler University, 2018.
  * [37] A.S. Nair.  Curtains in Cylindrical Algebraic Decomposition.  PhD thesis, University of Bath, 2021.  URL: https://researchportal.bath.ac.uk/en/studentTheses/curtains-in-cylindrical-algebraic-decomposition.
  * [38] Ali Kemal Uncu and Haniel Barbosa, editors.  Proceedings of the 7th SC-Square Workshop, volume 3458, 2023.  URL: https://ceur-ws.org/Vol-3458/.
  * [39] Ali Kemal Uncu, James H. Davenport, and Matthew England.  Smt-solving induction proofs of inequalities.  In Uncu and Barbosa [38], pages 10–24.  URL: https://ceur-ws.org/Vol-3458/paper2.pdf.
  * [40] F. Vale-Enriquez and C.W. Brown.  Polynomial Constraints and Unsat Cores in TARSKI.  In J.H. Davenport, M. Kauers, G. Labahn, and J. Urban, editors, Proceedings Mathematical Software — ICMS 2018, pages 466–474, 2018.  doi:10.1007/978-3-319-96418-8_55.
  * [41] B.L. van der Waerden.  Modern Algebra Vol. II (trans. Theodore J. Benac).  Frederick Ungar, 1950.
  * [42] B.L. van der Waerden.  Modern Algebra Vol. II (trans. F. Blum and J.R. Schulenberger).  Frederick Ungar, 1970.
  * [43] B.L. van der Waerden.  About [13].  Private communication to G.E. Collins, 1975.
  * [44] R.J. Walker.  Algebraic Curves.  Dover, 1962.