From 961e2a964d7b04ca069b89bb6f40f22ed18170a4 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 2 Jun 2017 21:52:43 -0400
Subject: [PATCH] bookvolbib reference for Cylindrical Algebraic Decomposition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Goal: Axiom Algebra
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@inproceedings{Hong90,
author = "Hong, Hoon",
title = "An improvement of the projection operator in cylindrical
algebraic decomposition",
booktitle = "ISSAC'90",
publisher = "ACM",
pages = "261-264",
year = "1990",
abstract =
"The cylindrical algebraic decomposition (CAD) of Collins (1975)
provides a potentially powerful method for solving many important
mathematical problems, provided that the required amount of
computation can be sufficiently reduced. An important component
of the CAD method is the projection operation. Given a set $A$ of
$r$-variate polynomials, the projection operation produces a
certain set $P$ of ($r − l$)-variate polynomials such that a CAD
of $r$-dimensional space for $A$ can be constructed from a CAD
of ($r − 1$)-dimensional space for $P$. The CAD algorithm begins
by applying the projection operation repeatedly, beginning
with the input polynomials, until univariate polynomials are
obtained. This process is called the projection phase.",
paper = "Hong90.pdf"
}
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@inproceedings{Hong98,
author = "Hong, Hoon",
title = "Simple Solution Formula Construction in Cylindrical
Algebraic Decomposition Based Quantifier Elimination",
booktitle = "Quantifier Elimination and Cylindrical Algebraic
Decomposition",
publisher = "Springer",
year = "1998",
isbn = "3-211-82794-3",
pages = "201-219",
comment = "also ISSAC'92 pages 177-188, 1992",
abstract =
"In this paper, we present several improvements to the last step
(solution formula construction step) of Collins' cylindrical
algebraic decomposition based quantifier elimination algorithm.
The main improvements are
\begin{itemize}
\item that it does {\sl not} use the expensive augmented projection
used by Collins' original algorithm, and
\item that it produces {\sl simple} solution formulas by using
three-valued logic minimization
\end{itemize}
For example, for the quadratic problem studied by Arnon, Mignotte,
and Lazard, the solution formula produced by the original algorithm
consists of 401 atomic formulas, but that by the improved algorithm
consists of 5 atomic formulas.",
paper = "Hong98.pdf"
}
\end{chunk}
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@phdthesis{Hong90a,
author = "Hong, Hoon",
title = "Improvements in CAD-based Quantifier Elimination",
institution = "Ohio State University",
year = "1990",
abstract =
"Many important mathematical and applied mathematical problems can be
formulated as quantifier elimination problems (QE) in elementary
algebra and geometry. Among several proposed QE methods, the best one
is the CAD-based method due to G. E. Collins. The major contributions
of this thesis are centered around improving each phase of the
CAD-based method: the projection phase, the truth-invariant CAD
construction phase, and the solution formula construction phase
Improvements in the projection phase. By generalizing a lemma on which
the proof of the original projection operation is based, we are able
to reduce the size of the projection set significantly, and thus speed
up the whole QE process.
Improvements in the truth-invariant CAD construction phase. By
intermingling the stack constructions with the truth evaluations, we
are usually able to complete quantifier elimination with only a
partially built CAD, resulting in significant speedup.
Improvements in the solution formula construction phase. By
constructing defining formulas for a collection of cells instead of
individual cells, we are often able to produce simple solution
formulas, without incurring the enormous cost of augmented projection.
The new CAD-based QE algorithm, which integrates all the improvements
above, has been implemented and tested on ten QE problems from diverse
application areas. The overall speedups range from 2 to perhaps
300,000 times at least
We also implemented D. Lazard's recent improvement on the projection
phase. Tests on the ten QE problems show additional speedups by up to
1.8 times."
}
\end{chunk}
\index{Collins, George E.}
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@article{Coll91,
author = "Collins, George E. and Hong, Hoon",
title = "Partial Cylindrical Algebraic Decomposition for Quantifier
Elimination",
journal = "J. Symbolic Computation",
year = "1991",
volume = "12",
pages = "299-328",
abstract =
"The Cylindrical Algebraic Decomposition method (CAD) decomposes $R^r$
into regions over which given polynomials have constant signs. An
important application of GAD is quantifier elimination in elementary
algebra and geometry. In this paper we present a method which
intermingles CAD construction with truth evaluation so that parts of
the CAD are constructed only as needed to further truth evaluation and
aborts CAD construction as soon as no more truth evaluation is needed.
The truth evaluation utilizes in an essential way any quantifiers
which are present and additionally takes account of atomic formulas
from which some variables are absent. Preliminary observations show
that the new method is always more efficient than the original, and
often significantly more efficient.",
paper = "Coll91.pdf"
}
\end{chunk}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@article{Mcca93,
author = "McCallum, Scott",
title = "Solving Polynomial Strict Inequalities Using Cylindrical
Algebraic Decomposition",
journal = "The Computer Journal",
volume = "36",
number = "5",
pages = "432-438",
year = "1993",
abstract =
"We consider the problem of determining the consistency over the real
number of a system of integral polynomial strict inequalities. This
problem has applications in geometric modelling. The cylindrical
algebraic decomposition (cad) algorithm [2] can be used to solve this
problem, though not very efficiently. In this paper we present a less
powerful version of the cad algorithm which can be used to solve the
consistency problem for conjunctions of strict inequalities, and which
runs considerably faster than the original method applied to this
problem. In the case that a given conjunction of strict inequalities
is consistent, the modified cad algorithm constructs solution points
with rational coordinates.",
paper = "Mcca93.pdf"
}
\end{chunk}
\index{Collins, George E.}
\begin{chunk}{axiom.bib}
@inproceedings{Coll98,
author = "Collins, George E.",
title = "Quantifier Elimination by Cylindrical Algebraic Decomposition --
Twenty Years of Progress",
booktitle = "Quantifier Elimination and Cylindrical Algebraic
Decomposition",
isbn = "3-211-82794-3",
year = "1998",
pages = "8-23",
abstract =
"The CAD (cylindrical algebraic decomposition) method and its
application to QE (quantifier elimination) for ERA (elementary real
algebra) was announced by the author in 1973 at Carnegie Mellon
University (Collins 1973b). In the twenty years since then several
very important improvements have been made to the method which,
together with a very large increase in available computational power,
have made it possible to solve in seconds or minutes some interesting
problems. In the following we survey these improvements and present
some of these problems with their solutions."
}
\end{chunk}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@article{Mcca02,
author = "McCallum, Scott",
title = "Local box adjacency algorithms for cylindrical algebraic
decompositions",
journal = "J. of Symbolic Computation",
volume = "33",
number = "3",
year = "2002",
pages = "321-342",
publisher = "Elsevier",
abstract =
"We describe new algorithms for determining the adjacencies between
zero-dimensional cells and those one-dimensional cells that are
sections (not sectors) in cylindrical algebraic decompositions
(cad). Such adjacencies constitute a basis for determining all other
cell adjacencies. Our new algorithms are local, being applicable to a
specified 0D cell and the 1D cells described by specified
polynomials. Particularly efficient algorithms are given for the 0D
cells in spaces of dimensions two, three and four. Then an algorithm
is given for a space of arbitrary dimension. This algorithm may on
occasion report failure, but it can then be repeated with a modified
isolating interval and a likelihood of success.",
paper = "Mcca02.pdf"
}
\end{chunk}
\index{Dolzmann, Andreas}
\index{Seidl, Andreas}
\index{Sturm, Thomas}
\begin{chunk}{axiom.bib}
@inproceedings{Dolz04,
author = "Dolzmann, Andreas and Seidl, Andreas and Sturm, Thomas",
title = "Efficient projection orders for CAD",
booktitle = "proc ISSAC'04",
year = "2004",
pages = "111-118",
publisher = "ACM",
isbn = "1-58113-827-X",
abstract =
"We introduce an efficient algorithm for determining a suitable
projection order for performing cylindrical algebraic
decomposition. Our algorithm is motivated by a statistical analysis of
comprehensive test set computations. This analysis introduces several
measures on both the projection sets and the entire computation, which
turn out to be highly correlated. The statistical data also shows that
the orders generated by our algorithm are significantly close to optimal.",
paper = "Doze04.pdf"
}
\end{chunk}
\index{Arnon, Dennis S.}
\index{Collins, George E.}
\index{McCallum, Scott}
\begin{chunk}{axiom.bib}
@article{Arno88b,
author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
title = "An Adjacency algorithm for cylindrical algebraic decompositions
of three-dimensional space",
journal = "J. Symbolic Computation",
volume = "5",
number = "1-2",
pages = "163-187",
year = "1988",
abstract =
"Let $A \subset \mathbb{Z}[x_1,\ldots,x_r]$
be a finite set. An {\sl A-invariant cylindrical
algebraic decomposition (cad)} is a certain partition of $r$-dimenslonal
euclidean space $E^r$ into semi-algebraic cells such that the value of
each $A_i \in A$ has constant sign (positive, negative, or zero)
throughout each cell. Two cells are adjacent if their union is
connected. We give an algorithm that determines the adjacent pairs
of cells as it constructs a cad of $E^3$. The general teehnlque
employed for $^3$ adjacency determination is “projection” into $E^2$,
followed by application of an existing $E^2$ adjacency elgorlthm
(Arnon, Collins, McCallum, 1984). Our algorithm has the following
properties: (1) it requires no coordinate changes, end (2) in any
cad of $E^1$, $E^2$, or $E^3$ that it builds, the boundary of each cell
is a (disjoint) union of lower-dlmenaionel cells.",
paper = "Arno88b.pdf"
}
\end{chunk}
\index{Ben-Or, Michael}
\index{Kozen, Dexter}
\index{Reif, John}
\begin{chunk}{axiom.bib}
@article{Beno86,
author = "Ben-Or, Michael and Kozen, Dexter and Reif, John",
title = "The complexity of elementary algebra and geometry",
journal = "J. Computer and System Sciences",
volume = "32",
number = "2",
year = "1986",
pages = "251-264",
abstract =
"The theory of real closed fields can be decided in exponential space
or parallel exponential time. In fixed dimesnion, the theory can be
decided in NC.",
paper = "Beno86.pdf"
}
\end{chunk}
\index{Fitchas, N.}
\index{Galligo, A.}
\index{Morgenstern, J.}
\begin{chunk}{axiom.bib}
@techreport{Fitc87,
author = "Fitchas, N. and Galligo, A. and Morgenstern, J.",
title = {Algorithmes repides en s\'equential et en parallele pour
l'\'elimination de quantificateurs en g\'eom\'etrie
\'el\'ementaire},
type = "technical report",
institution = {UER de Math\'ematiques Universite de Paris VII},
year = "1987"
}
\end{chunk}
\index{Grigor'ev, D. Yu.}
\index{Vorobjov, N. N.}
\begin{chunk}{axiom.bib}
@article{Grig88,
author = "Grigor'ev, D. Yu. and Vorobjov, N. N.",
title = "Solving systems of polynomial inequalities in subexponential time",
journal = "J. Symbolic Computation",
volume = "5",
number = "1-2",
pages = "37-64",
year = "1988"
abstract =
"Let the polynomials $f_1,\ldots,f_k \in \mathbb{Z}[X_1,\ldots,X_n]$
have degrees $deg(f_i) 0,\ldots,f_k \ge 0$. In the case of a positive
answer the algorithm constructs a certain finite set of solutions
(which is, in fact, a representative set for the family of components
of connectivity of the set of all real solutions of the system). The
algorithm runs in time polynomial in $M(kd)^{n^2}$. The previously
known upper time bound for this problem was $(Mkd)^{2^{O(n)}}$.",
paper = "Grig88.pdf"
}
\end{chunk}
\index{Canny, John}
\begin{chunk}{axiom.bib}
@inproceedings{Cann88,
author = "Canny, John",
title = "Some algebraic and geometric computations in PSPACE",
booktitle = "Proc 20th ACM Symp. on the theory of computing",
pages = "460-467",
year = "1988",
isbn = "0-89791-264-0",
link = "\url{http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-88-439.pdf}",
abstract =
"We give a PSPACE algorithm for determining the signs of multivariate
polynomials at the common zeros of a system of polynomial
equations. One of the consequences of this result is that the
``Generalized Movers' Problem'' in robotics drops from EXPTIME into
PSPACE, and is therefore PSPACE-complete by a previous hardness result
[Rei]. We also show that the existential theory of the real numbers
can be decided in PSPACE. Other geometric problems that also drop into
PSPACE include the 3-d Euclidean Shortest Path Problem, and the ``2-d
Asteroid Avoidance Problem'' described in [RS]. Our method combines the
theorem of the primitive element from classical algebra with a
symbolic polynomial evaluation lemma from [BKR]. A decision problem
involving several algebraic numbers is reduced to a problem involving
a single algebraic number or primitive element, which rationally
generates all the given algebraic numbers.",
paper = "Cann88.pdf"
}
\end{chunk}
\index{Canny, John}
\begin{chunk}{axiom.bib}
@article{Cann93,
author = "Canny, John",
title = "Improved algorithms for sign and existential quantifier
elimination",
journal = "The Computer Journal",
volume = "36",
pages = "409-418",
year = "1993",
abstract =
"Recently there has been a lot of activity in algorithms that work
over real closed fields, and that perform such calculations as
quantifier elimination or computing connected components of
semi-algebraic sets. A cornerstone of this work is a symbolic sign
determination algorithm due to Ben-Or, Kozen and Reif. In this
paper we describe a new sign determination method based on the earlier
algorithm, but with two advantages: (i) It is faster in the univariate
case, and (ii) In the general case, it allows purely symbolic
quantifier elimination in pseudo-polynomial time. By purely symbolic,
we mean that it is possible to eliminate a quantified variable from a
system of polynomials no matter what the coefficient values are. The
previous methods required the coefficients to be themselves
polynomials in other variables. Our new method allows transcendental
functions or derivatives to appear in the coefficients.
Another corollary of the new sign-determination algorithm is a very
simple, practical algorithm for deciding existentially-quantified
formulae of the theory of the reals. We present an algorithm that has
a bit complexity of $n^{k+1}d^{O(k)}(c log n)^{1+\epsilon}$ randomized, or
$n^{n+1}d^{O(k^2)}c(1+\epsilon)$ deterministic, for any
$\epsilon>0$, where $n$ is the number
of polynomial constraints in the defining formula, $k$ is the number of
variables, $d$ is a bound on the degree, $c$ bounds the bit length of the
coefficient. The algorithm makes no general position assumptions, and
its constants are much smaller than other recent quantifier
elimination methods.",
paper = "Cann93.pdf"
}
\end{chunk}
\index{Heintz, J.}
\index{Roy, M-F.}
\index{Solerno, P.}
\begin{chunk}{axiom.bib}
@inproceedings{Hein89,
author = "Heintz, J. and Roy, M-F. and Solerno, P.",
title = "On the complexity of semialgebraic sets",
booktitle = "Proc. IFIP",
pages = "293-298",
year = "1989"
}
\end{chunk}
\index{Renegar, James}
\begin{chunk}{axiom.bib}
@article{Rene92,
author = "Renegar, James",
title = "On the computational complexity and geometry of the first-order
theory of the reals. Part I: Introduction"
journal = "J. of Symbolic Computation",
volume = "13",
number = "3",
year = "1992",
pages = "255-299",
link =
"\url{http://www.sciencedirect.com/science/article/pii/S0747717110800033}",
abstract =
"This series of papers presents a complete development and complexity
analysis of a decision method, and a quantifier elimination method,
for the first order theory of the reals. The complexity upper bounds
which are established are the best presently available, both for
sequential and parallel computation, and both for the bit model of
computation and the real number model of computation; except for the
bounds pertaining to the sequential decision method in the bit model
of computation, all bounds represent significant improvements over
previously established bounds.",
paper = "Rene92.pdf"
}
\end{chunk}
\index{Renegar, James}
\begin{chunk}{axiom.bib}
@article{Rene92a,
author = "Renegar, James",
title = "On the computational complexity and geometry of the first-order
theory of the reals. Part II: The general decision problem"
journal = "J. of Symbolic Computation",
volume = "13",
number = "3",
year = "1992",
pages = "301-327",
link =
"\url{http://www.sciencedirect.com/science/article/pii/S0747717110800045}",
abstract =
"This series of papers presents a complete development and complexity
analysis of a decision method, and a quantifier elimination method,
for the first order theory of the reals. The complexity upper bounds
which are established are the best presently available, both for
sequential and parallel computation, and both for the bit model of
computation and the real number model of computation; except for the
bounds pertaining to the sequential decision method in the bit model
of computation, all bounds represent significant improvements over
previously established bounds.",
paper = "Rene92a.pdf"
}
\end{chunk}
\index{Renegar, James}
\begin{chunk}{axiom.bib}
@article{Rene92b,
author = "Renegar, James",
title = "On the computational complexity and geometry of the first-order
theory of the reals. Part III: Quantifier elimination"
journal = "J. of Symbolic Computation",
volume = "13",
number = "3",
year = "1992",
pages = "329-352",
link =
"\url{http://www.sciencedirect.com/science/article/pii/S0747717110800057}",
abstract =
"This series of papers presents a complete development and complexity
analysis of a decision method, and a quantifier elimination method,
for the first order theory of the reals. The complexity upper bounds
which are established are the best presently available, both for
sequential and parallel computation, and both for the bit model of
computation and the real number model of computation; except for the
bounds pertaining to the sequential decision method in the bit model
of computation, all bounds represent significant improvements over
previously established bounds.",
paper = "Rene92b.pdf"
}
\end{chunk}
\index{Arnon, Dennis S.}
\begin{chunk}{axiom.bib}
@article{Arno88c,
author = "Arnon, Dennis S.",
title = "A bibliography of quantifier elimination for real closed fields",
journal = "J. of Symbolic Computation",
volume = "5",
number = "1-2",
pages = "267-274",
year = "1988",
link =
"\url{http://www.sciencedirect.com/science/article/pii/S0747717188800166}",
abstract =
"A basic collection of literature relating to algorithmic quantifier
elimination for real closed fields is assembled",
paper = "Arno88c.pdf"
}
\end{chunk}
\index{Seidenberg, A.}
\begin{chunk}{axiom.bib}
@article{Seid54,
author = "Seidenberg, A.",
title = "A New Decision Method for Elementary Algebra",
journal = "Annals of Mathematics",
volume = "60",
number = "2",
year = "1954",
pages = "365-374",
abstract =
"A. Tarski [4] has given a decision method for elementary algebra. In
essence this comes to giving an algorithm for deciding whether a
given finite set of polynomial inequalities has a solution. Below we
offer another proof of this result of Tarski. The main point of our
proof is accomplished upon showing how to decide whether a given
polynomial $f(x,y)$ in two variables, defined over the field \mathbb{R}
o rational numbers, has a zero in a real-closed field \mathbb{K}
containing $R^1$.
This is done in \S{}2, but for purposes of induction it is necessary to
consider also the case that the coefficients of $f(x,y)$ involve
parameters; the remarks in \S{}3 will be found sufficient for this
point. In \S{}1, the problem is reduced to a decision for equalities,
but an induction (on the number of unknowns) could not possibly be
carried out on equalities alone; we consider a simultaneous system
consisting of one equality $f(x,y) = 0$ and one inequality $F(x) \ne 0$.
Once the decision for this case is achieved, at least as in \S{}3,
the induction is immediate.",
paper = "Seid54.pdf"
}
\end{chunk}
\index{Weispfenning, V.}
\begin{chunk}{axiom.bib}
@articl{Weis92,
author = "Weispfenning, V.",
title = "Comprehensive Groebner bases",
journal = "J. Symbolic Computation",
volume = "14",
number = "1",
year = "1992",
pages = "1-29",
abstract =
"Let $K$ be an integral domain and let $S$ be the polynomial ring
$K[U_1,\ldots,U_m; X_1,\ldots,X_n]$. For any finite $F \subseteq S$,
we construct a comprehensive Groebner basis of the ideal $Id(F)$, a
finite ideal basis of $Id(F)$ that is a Groebner basis of $Id(F)$
in $K^\prime[X_1,\ldots,X_n]$ for every specialization of the
parameters $U_1,\ldots,U_m$ in an arbitrary field $K^1$. We show
that this construction can be performed with the same worst case
degree bounds in the main variable $X_i$, as for ordinary Groebner
bases; moreover, examples computed in an ALDES/SAC-2 implementation
show that the construction is of practical value. Comprehensive
Groebner bases admit numerous applications to parametric problems
in algebraic geometry; in particular, they yield a fast elimination
of quantifier-blocks in algebraically closed fields",
paper = "Weis92.pdf"
}
\end{chunk}
\index{Canny, John}
\begin{chunk}{axiom.bib}
@inproceeding{Cann87,
author = "Canny, John",
title = "A new algebraic method of robot motion planning and real geometry",
booktitle = "IEEE Symp. on Foundations of Comp. Sci.",
pages = "39-48",
abstract =
"We present an algorithm which solves the findpath or generalized
movers' problem in single exponential sequential time. This is the
first algorithm for the problem whose sequential time bound is less
than double exponential. In fact, the combinatorial exponent of the
algorithm is equal to the number of degrees of freedom, making it
worst-case optimal, and equaling or improving the time bounds of many
special purpose algorithms. The algorithm accepts a formula for a
semi-algebraic set S describing the set of free configurations and
produces a one-dimensional skeleton or ``roadmap'' of the set, which is
connected within each connected component of S. Additional points may
be linked to the roadmap in linear time. Our method draws from results
of singularity theory, and in particular makes use of the notion of
stratified sets as an efficient alternative to cell decomposition. We
introduce an algebraic tool called the multivariate resultant which
gives a necessary and sufficient condition for a system of homogeneous
polynomials to have a solution, and show that it can be computed in
polynomial parallel time. Among the consequences of this result are
new methods for quantifier elimination and an improved gap theorem for
the absolute value of roots of a system of polynomials.",
paper = "Cann87.pdf"
}
\end{chunk}
\index{Pedersen, P.}
\index{Roy, F.-F.}
\index{Szpirglas, A.}
\begin{chunk}{axiom.bib}
@inproceeding{Pede93,
author = "Pedersen, P. and Roy, F.-F. and Szpirglas, A.",
title = "Counting real zeroes in the multivariate case",
booktitle = "Proc. MEGA'92: Computational Algebraic Geometry",
volume = "109",
pages = "203-224",
year = "1993",
abstract =
"In this paper we show, by generalizing Hermite’s theorem to the
multivariate setting, how to count the number of real or complex
points of a discrete algebraic set which lie within some algebraic
constraint region. We introduce a family of quadratic forms determined
by the algebraic constraints and defined in terms of the trace from
the coordinate ring of the variety to the ground field, and we show
that the rank and signature of these forms are sufficient to determine
the number of real points lying within a constraint region. In all
cases we count geometric points, which is to say, we count points
without multiplicity. The theoretical results on these quadratic forms
are more or less classical, but forgotten too, and can be found also
in [3].
We insist on effectivity of the computation and complexity analysis:
we show how to calculate the trace and signature using Gröbner bases,
and we show how the information provided by the individual quadratic
forms may be combined to determine the number of real points
satisfying a conjunction of constraints. The complexity of the
computation is polynomial in the dimension as a vector space of the
quotient ring associated to the defining equations. In terms of the
number of variables, the complexity of the computation is singly
exponential. The algorithm is well parallelizable.
We conclude the paper by applying our machinery to the problem of
effectively calculating the Euler characteristic of a smooth
hypersurface."
}
\end{chunk}
\index{Weispfenning, V.}
\begin{chunk}{axiom.bib}
@articl{Weis88,
author = "Weispfenning, V.",
title = "The complexity of linear problems in fields",
journal = "J. of Symbolic Computation",
volume = "5",
number = "1-2",
year = "1988",
pages = "3-27",
link = "\url{http://www.sciencedirect.com.proxy.library.cmu.edu/science/article/pii/S0747717188800038}",
abstract =
"We consider linear problems in fields, ordered fields, discretely
valued fields (with finite residue field or residue field of
characteristic zero) and fields with finitely many independent
orderings and discrete valuations. Most of the fields considered will
be of characteristic zero. Formally, linear statements about these
structures (with parameters) are given by formulas of the respective
first-order language, in which all bound variables occur only
linearly. We study symbolic algorithms
({\sl linear elimination procedures})
that reduce linear formulas to linear formulas of a very simple form,
i.e. quantifier-free linear formulas, and algorithms
({\sl linear decision procedures})
that decide whether a given linear sentence holds in all
structures of the given class. For all classes of fields considered,
we find linear elimination procedures that run in double exponential
space and time. As a consequence, we can show that for fields (with
one or several discrete valuations), linear statements can be
transferred from characteristic zero to prime characteristic $p$,
provided $p$ is double exponential in the length of the statement. (For
similar bounds in the non-linear case, see Brown, 1978.) We find
corresponding linear decision procedures in the Berman complexity
classes $\bigcup_{c\in N} STA(*,2^{cn},dn)$
for $d = 1, 2$. In particular, all these procedures run in
exponential space. The technique employed is quantifier elimination
via Skolem terms based on Ferrante & Rackoff (1975). Using ideas of
Fischer & Rabin (1974), Berman (1977), Fürer (1982), we establish
lower bounds for these problems showing that our upper bounds are
essentially tight. For linear formulas with a bounded number of
quantifiers all our algorithms run in polynomial time. For linear
formulas of bounded quantifier alternation most of the algorithms run
in time $2^{O(n^k)} for fixed $k$.",
paper = "Weis88.pdf"
}
\end{chunk}
\index{Weispfenning, V.}
\begin{chunk}{axiom.bib}
@inproceedings{Weis94,
author = "Weispfenning, V.",
title = "Quantifier elimination for real algebra – the cubic case",
booktitle = "Proc ISSAC'94",
publisher = "ACM",
isbn = "0-89791-638-7",
pages = "258-263",
year = "1994",
abstract =
"We present a special purpose quantifier elimination method that
eliminates a quantifier $\exists x$ in formulas $\exists x(\rho)$
where $\rho$ is a boolean combination of polynomial inequalities of
degree $\le 3$ with respect to $x$. The method extends the virtual
substitition of parameterized test points developed in
[Weispfenning 1, Loos and Weispf.] for the linear case and in
[Weispfenning 2] for the quadratic case. It has similar upper
complexity bounds and offers similar advantages (relatively large
preprocessing part, explicit parametric solutions). Small examples
suggest that the method will be of practical significance.",
paper = "Weis94.pdf"
}
\end{chunk}
\index{Loos, Rudiger}
\index{Weispfenning, Volker}
\begin{chunk}{axiom.bib}
@article{Loos93,
author = "Loos, Rudiger and Weispfenning, Volker",
title = "Applying linear quantifier elimination",
journal = "The Computer Journal",
volume = "36",
number = "5",
year = "1993",
abstract =
"The linear quantifier elimination algorithm for ordered fields in
[15] is applicable to a wide range of examples involving even
non-linear parameters. The Skolem sets of the original algorithm
are generalized to elimination sets whose size is linear in the
number of atomic formulas, whereas the size of Skolem sets is
quadratic in this number. Elimiation sets may contain non-standard
terms which enter the computation symoblically. Many cases can be
treated by special methods improving further the empirical computing
times.",
paper = "Loos93.pdf"
}
\end{chunk}
\index{Anai, Hirokazu}
\index{Weispfenning, Volker}
\begin{chunk}{axiom.bib}
@inproceedings{Anai00,
author = "Anai, Hirokazu and d{Weispfenning, Volker",
title = "Deciding linear-trigonometric problems",
booktitle = "Proc ISSAC'00",
publisher = "ACM",
isbn = "1-58113-218-2",
year = "2000",
pages = "14-22",
abstract =
"In this paper, we present a decision procedure for certain
linear-trigonometric problems for the reals and integers formalized in
a suitable first-order language. The inputs are restricted to
formulas, where all but one of the quantified variables occur linearly
and at most one occurs both linearly and in a specific trigonometric
function. Moreover we may allow in addition the integer-part operation
in formulas. Besides ordinary quantifiers, we allow also counting
quantifiers. Furthermore we also determine the qualitative structure
of the connected components of the satisfaction set of the mixed
linear-trigonometric variable. We also consider the decision of these
problems in subfields of the real algebraic numbers.",
paper = "Anai00.pdf"
}
\end{chunk}
---
books/bookvolbib.pamphlet | 929 +++++++++++++++++++++++++++++++++++++++-
changelog | 2 +
patch | 792 ++++++++++++++++++++++++++++++++++-
src/axiom-website/patches.html | 4 +-
4 files changed, 1719 insertions(+), 8 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 2c0a27b..2b0a9ee 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -936,8 +936,8 @@ paragraph for those unfamiliar with the terms.
\begin{chunk}{axiom.bib}
@Article{Come12,
author = "Comer, Matthew T. and Kaltofen, Erich L.",
- title = "On the {Berlekamp}/{Massey} Algorithm and Counting Singular {Hankel}
- Matrices over a Finite Field",
+ title = "On the {Berlekamp}/{Massey} Algorithm and Counting Singular
+ {Hankel} Matrices over a Finite Field",
year = "2012",
month = "April",
journal = "Journal of Symbolic Computation",
@@ -4461,7 +4461,7 @@ when shown in factored form.
\index{Kagstrom, Bo}
\index{Poromaa, Peter}
\begin{chunk}{axiom.bib}
-@article{Kags93,
+@techreport{Kags93,
author = "Kagstrom, Bo and Poromaa, Peter",
title = "LAPACK-Style Algorithms and Software for Solving the Generalized
Sylvester Equation and Estimating the Separation between
@@ -14511,6 +14511,34 @@ Proc ISSAC 97 pp172-175 (1997)
\subsection{A} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Anai, Hirokazu}
+\index{Weispfenning, Volker}
+\begin{chunk}{axiom.bib}
+@inproceedings{Anai00,
+ author = "Anai, Hirokazu and Weispfenning, Volker",
+ title = "Deciding linear-trigonometric problems",
+ booktitle = "Proc ISSAC'00",
+ publisher = "ACM",
+ isbn = "1-58113-218-2",
+ year = "2000",
+ pages = "14-22",
+ abstract =
+ "In this paper, we present a decision procedure for certain
+ linear-trigonometric problems for the reals and integers formalized in
+ a suitable first-order language. The inputs are restricted to
+ formulas, where all but one of the quantified variables occur linearly
+ and at most one occurs both linearly and in a specific trigonometric
+ function. Moreover we may allow in addition the integer-part operation
+ in formulas. Besides ordinary quantifiers, we allow also counting
+ quantifiers. Furthermore we also determine the qualitative structure
+ of the connected components of the satisfaction set of the mixed
+ linear-trigonometric variable. We also consider the decision of these
+ problems in subfields of the real algebraic numbers.",
+ paper = "Anai00.pdf"
+}
+
+\end{chunk}
+
\index{Arnon, Dennis Soul\'e}
\begin{chunk}{axiom.bib}
@phdthesis{Arno81,
@@ -14618,7 +14646,6 @@ Proc ISSAC 97 pp172-175 (1997)
volume = "5",
pages = "237-259",
year = "1988",
- link = "\url{http://http://www.sciencedirect.com/science/article/pii/S0747717188800142/pdf?md5=62052077d84e6078cc024bc8e29c23c1&pid=1-s2.0-S0747717188800142-main.pdf}",
abstract = "
We give solutions to two problems of elementary algebra and geometry:
(1) find conditions on real numbers $p$, $q$, and $r$ so that the
@@ -14641,8 +14668,8 @@ Proc ISSAC 97 pp172-175 (1997)
\index{Arnon, Dennis}
\index{Buchberger, Bruno}
-@misc{Arno88a,
\begin{chunk}{axiom.bib}
+@misc{Arno88a,
author = "Arnon, Dennis and Buchberger, Bruno",
title = "Algorithms in Real Algebraic Geometry",
publisher = "Academic Press",
@@ -14652,6 +14679,59 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\index{Arnon, Dennis S.}
+\index{Collins, George E.}
+\index{McCallum, Scott}
+\begin{chunk}{axiom.bib}
+@article{Arno88b,
+ author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
+ title = "An Adjacency algorithm for cylindrical algebraic decompositions
+ of three-dimensional space",
+ journal = "J. Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ pages = "163-187",
+ year = "1988",
+ abstract =
+ "Let $A \subset \mathbb{Z}[x_1,\ldots,x_r]$
+ be a finite set. An {\sl A-invariant cylindrical
+ algebraic decomposition (cad)} is a certain partition of $r$-dimenslonal
+ euclidean space $E^r$ into semi-algebraic cells such that the value of
+ each $A_i \in A$ has constant sign (positive, negative, or zero)
+ throughout each cell. Two cells are adjacent if their union is
+ connected. We give an algorithm that determines the adjacent pairs
+ of cells as it constructs a cad of $E^3$. The general teehnlque
+ employed for $^3$ adjacency determination is “projection” into $E^2$,
+ followed by application of an existing $E^2$ adjacency elgorlthm
+ (Arnon, Collins, McCallum, 1984). Our algorithm has the following
+ properties: (1) it requires no coordinate changes, end (2) in any
+ cad of $E^1$, $E^2$, or $E^3$ that it builds, the boundary of each cell
+ is a (disjoint) union of lower-dlmenaionel cells.",
+ paper = "Arno88b.pdf"
+}
+
+\end{chunk}
+
+\index{Arnon, Dennis S.}
+\begin{chunk}{axiom.bib}
+@article{Arno88c,
+ author = "Arnon, Dennis S.",
+ title = "A bibliography of quantifier elimination for real closed fields",
+ journal = "J. of Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ pages = "267-274",
+ year = "1988",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717188800166}",
+ abstract =
+ "A basic collection of literature relating to algorithmic quantifier
+ elimination for real closed fields is assembled",
+ paper = "Arno88c.pdf"
+}
+
+\end{chunk}
+
\subsection{B} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Baker, Henry G.}
@@ -14757,6 +14837,27 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\index{Ben-Or, Michael}
+\index{Kozen, Dexter}
+\index{Reif, John}
+\begin{chunk}{axiom.bib}
+@article{Beno86,
+ author = "Ben-Or, Michael and Kozen, Dexter and Reif, John",
+ title = "The complexity of elementary algebra and geometry",
+ journal = "J. Computer and System Sciences",
+ volume = "32",
+ number = "2",
+ year = "1986",
+ pages = "251-264",
+ abstract =
+ "The theory of real closed fields can be decided in exponential space
+ or parallel exponential time. In fixed dimesnion, the theory can be
+ decided in NC.",
+ paper = "Beno86.pdf"
+}
+
+\end{chunk}
+
\index{Bradford, Russell}
\index{Chen, Changbo}
\index{Davenport, James H.}
@@ -14980,6 +15081,111 @@ Proc ISSAC 97 pp172-175 (1997)
\subsection{C} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@inproceedings{Cann87,
+ author = "Canny, John",
+ title = "A new algebraic method of robot motion planning and real geometry",
+ booktitle = "IEEE Symp. on Foundations of Comp. Sci.",
+ pages = "39-48",
+ year = "1987",
+ abstract =
+ "We present an algorithm which solves the findpath or generalized
+ movers' problem in single exponential sequential time. This is the
+ first algorithm for the problem whose sequential time bound is less
+ than double exponential. In fact, the combinatorial exponent of the
+ algorithm is equal to the number of degrees of freedom, making it
+ worst-case optimal, and equaling or improving the time bounds of many
+ special purpose algorithms. The algorithm accepts a formula for a
+ semi-algebraic set S describing the set of free configurations and
+ produces a one-dimensional skeleton or ``roadmap'' of the set, which is
+ connected within each connected component of S. Additional points may
+ be linked to the roadmap in linear time. Our method draws from results
+ of singularity theory, and in particular makes use of the notion of
+ stratified sets as an efficient alternative to cell decomposition. We
+ introduce an algebraic tool called the multivariate resultant which
+ gives a necessary and sufficient condition for a system of homogeneous
+ polynomials to have a solution, and show that it can be computed in
+ polynomial parallel time. Among the consequences of this result are
+ new methods for quantifier elimination and an improved gap theorem for
+ the absolute value of roots of a system of polynomials.",
+ paper = "Cann87.pdf"
+}
+
+\end{chunk}
+
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@inproceedings{Cann88,
+ author = "Canny, John",
+ title = "Some algebraic and geometric computations in PSPACE",
+ booktitle = "Proc 20th ACM Symp. on the theory of computing",
+ pages = "460-467",
+ year = "1988",
+ isbn = "0-89791-264-0",
+ link = "\url{http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-88-439.pdf}",
+ abstract =
+ "We give a PSPACE algorithm for determining the signs of multivariate
+ polynomials at the common zeros of a system of polynomial
+ equations. One of the consequences of this result is that the
+ ``Generalized Movers' Problem'' in robotics drops from EXPTIME into
+ PSPACE, and is therefore PSPACE-complete by a previous hardness result
+ [Rei]. We also show that the existential theory of the real numbers
+ can be decided in PSPACE. Other geometric problems that also drop into
+ PSPACE include the 3-d Euclidean Shortest Path Problem, and the ``2-d
+ Asteroid Avoidance Problem'' described in [RS]. Our method combines the
+ theorem of the primitive element from classical algebra with a
+ symbolic polynomial evaluation lemma from [BKR]. A decision problem
+ involving several algebraic numbers is reduced to a problem involving
+ a single algebraic number or primitive element, which rationally
+ generates all the given algebraic numbers.",
+ paper = "Cann88.pdf"
+}
+
+\end{chunk}
+
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@article{Cann93,
+ author = "Canny, John",
+ title = "Improved algorithms for sign and existential quantifier
+ elimination",
+ journal = "The Computer Journal",
+ volume = "36",
+ pages = "409-418",
+ year = "1993",
+ abstract =
+ "Recently there has been a lot of activity in algorithms that work
+ over real closed fields, and that perform such calculations as
+ quantifier elimination or computing connected components of
+ semi-algebraic sets. A cornerstone of this work is a symbolic sign
+ determination algorithm due to Ben-Or, Kozen and Reif. In this
+ paper we describe a new sign determination method based on the earlier
+ algorithm, but with two advantages: (i) It is faster in the univariate
+ case, and (ii) In the general case, it allows purely symbolic
+ quantifier elimination in pseudo-polynomial time. By purely symbolic,
+ we mean that it is possible to eliminate a quantified variable from a
+ system of polynomials no matter what the coefficient values are. The
+ previous methods required the coefficients to be themselves
+ polynomials in other variables. Our new method allows transcendental
+ functions or derivatives to appear in the coefficients.
+
+ Another corollary of the new sign-determination algorithm is a very
+ simple, practical algorithm for deciding existentially-quantified
+ formulae of the theory of the reals. We present an algorithm that has
+ a bit complexity of $n^{k+1}d^{O(k)}(c log n)^{1+\epsilon}$ randomized, or
+ $n^{n+1}d^{O(k^2)}c(1+\epsilon)$ deterministic, for any
+ $\epsilon>0$, where $n$ is the number
+ of polynomial constraints in the defining formula, $k$ is the number of
+ variables, $d$ is a bound on the degree, $c$ bounds the bit length of the
+ coefficient. The algorithm makes no general position assumptions, and
+ its constants are much smaller than other recent quantifier
+ elimination methods.",
+ paper = "Cann93.pdf"
+}
+
+\end{chunk}
+
\index{Caviness, B. F.}
\index{Johnson, J. R.}
\begin{chunk}{axiom.bib}
@@ -15122,6 +15328,86 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\index{Collins, George E.}
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
+@article{Coll91,
+ author = "Collins, George E. and Hong, Hoon",
+ title = "Partial Cylindrical Algebraic Decomposition for Quantifier
+ Elimination",
+ journal = "J. Symbolic Computation",
+ year = "1991",
+ volume = "12",
+ pages = "299-328",
+ abstract =
+ "The Cylindrical Algebraic Decomposition method (CAD) decomposes $R^r$
+ into regions over which given polynomials have constant signs. An
+ important application of GAD is quantifier elimination in elementary
+ algebra and geometry. In this paper we present a method which
+ intermingles CAD construction with truth evaluation so that parts of
+ the CAD are constructed only as needed to further truth evaluation and
+ aborts CAD construction as soon as no more truth evaluation is needed.
+ The truth evaluation utilizes in an essential way any quantifiers
+ which are present and additionally takes account of atomic formulas
+ from which some variables are absent. Preliminary observations show
+ that the new method is always more efficient than the original, and
+ often significantly more efficient.",
+ paper = "Coll91.pdf"
+}
+
+\end{chunk}
+
+\index{Collins, George E.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Coll98,
+ author = "Collins, George E.",
+ title = "Quantifier Elimination by Cylindrical Algebraic Decomposition --
+ Twenty Years of Progress",
+ booktitle = "Quantifier Elimination and Cylindrical Algebraic
+ Decomposition",
+ isbn = "3-211-82794-3",
+ year = "1998",
+ pages = "8-23",
+ abstract =
+ "The CAD (cylindrical algebraic decomposition) method and its
+ application to QE (quantifier elimination) for ERA (elementary real
+ algebra) was announced by the author in 1973 at Carnegie Mellon
+ University (Collins 1973b). In the twenty years since then several
+ very important improvements have been made to the method which,
+ together with a very large increase in available computational power,
+ have made it possible to solve in seconds or minutes some interesting
+ problems. In the following we survey these improvements and present
+ some of these problems with their solutions."
+}
+
+\end{chunk}
+
+\index{Collins, George E.}
+\index{Johnson, Jeremy R.}
+\index{Krandick, Werner}
+\begin{chunk}{axiom.bib}
+@article{Coll02,
+ author = "Collins, George E. and Johnson, Jeremy R. and Krandick, Werner",
+ title = "Interval arithmetic in cylindrical algebraic decomposition",
+ journal = "J. Symbolic Computation",
+ volume = "34",
+ number = "2",
+ pages = "145-157",
+ year = "2002",
+ publisher = "Elsevier",
+ abstract =
+ "Cylindrical algebraic decomposition requires many very time consuming
+ operations, including resultant computation, polynomial factorization,
+ algebraic polynomial gcd computation and polynomial real root
+ isolation. We show how the time for algebraic polynomial real root
+ isolation can be greatly reduced by using interval arithmetic instead
+ of exact computation. This substantially reduces the overall time for
+ cylindrical algebraic decomposition.",
+ paper = "Coll02.pdf"
+}
+
+\end{chunk}
+
\subsection{D} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Davenport, J.H.}
@@ -15172,6 +15458,31 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\index{Dolzmann, Andreas}
+\index{Seidl, Andreas}
+\index{Sturm, Thomas}
+\begin{chunk}{axiom.bib}
+@inproceedings{Dolz04,
+ author = "Dolzmann, Andreas and Seidl, Andreas and Sturm, Thomas",
+ title = "Efficient projection orders for CAD",
+ booktitle = "proc ISSAC'04",
+ year = "2004",
+ pages = "111-118",
+ publisher = "ACM",
+ isbn = "1-58113-827-X",
+ abstract =
+ "We introduce an efficient algorithm for determining a suitable
+ projection order for performing cylindrical algebraic
+ decomposition. Our algorithm is motivated by a statistical analysis of
+ comprehensive test set computations. This analysis introduces several
+ measures on both the projection sets and the entire computation, which
+ turn out to be highly correlated. The statistical data also shows that
+ the orders generated by our algorithm are significantly close to optimal.",
+ paper = "Doze04.pdf"
+}
+
+\end{chunk}
+
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{RealClosure}
@@ -15341,8 +15652,198 @@ Proc ISSAC 97 pp172-175 (1997)
\end{chunk}
+\subsection{F} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Fitchas, N.}
+\index{Galligo, A.}
+\index{Morgenstern, J.}
+\begin{chunk}{axiom.bib}
+@techreport{Fitc87,
+ author = "Fitchas, N. and Galligo, A. and Morgenstern, J.",
+ title = {Algorithmes repides en s\'equential et en parallele pour
+ l'\'elimination de quantificateurs en g\'eom\'etrie
+ \'el\'ementaire},
+ type = "technical report",
+ institution = {UER de Math\'ematiques Universite de Paris VII},
+ year = "1987"
+}
+
+\end{chunk}
+
+\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Grigor'ev, D. Yu.}
+\index{Vorobjov, N. N.}
+\begin{chunk}{axiom.bib}
+@article{Grig88,
+ author = "Grigor'ev, D. Yu. and Vorobjov, N. N.",
+ title = "Solving systems of polynomial inequalities in subexponential time",
+ journal = "J. Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ pages = "37-64",
+ year = "1988",
+ abstract =
+ "Let the polynomials $f_1,\ldots,f_k \in \mathbb{Z}[X_1,\ldots,X_n]$
+ have degrees $deg(f_i) 0,\ldots,f_k \ge 0$. In the case of a positive
+ answer the algorithm constructs a certain finite set of solutions
+ (which is, in fact, a representative set for the family of components
+ of connectivity of the set of all real solutions of the system). The
+ algorithm runs in time polynomial in $M(kd)^{n^2}$. The previously
+ known upper time bound for this problem was $(Mkd)^{2^{O(n)}}$.",
+ paper = "Grig88.pdf"
+}
+
+\end{chunk}
+
+\index{Grigor'ev, D. Yu.}
+\begin{chunk}{axiom.bib}
+@article{Grig88a,
+ author = "Grigor'ev, D. Yu.",
+ title = "The complexity of deciding Tarski algebra",
+ journal = "J. Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ pages = "65-108",
+ year = "1988",
+ abstract =
+ "Let a formula of Tarski algebra contain $k$ atomic subformulas of the
+ kind $(f_i \ge 0)$, $1 \le i \le k$, where the polynomials
+ $f_i \in \mathbb{Z}[X_1,\ldots,X_n]$ have degrees $deg(f_i) 0,\ldots,f_k \ge 0$. In the case of a positive
+ answer the algorithm constructs a certain finite set of solutions
+ (which is, in fact, a representative set for the family of components
+ of connectivity of the set of all real solutions of the system). The
+ algorithm runs in time polynomial in $M(kd)^{n^2}$. The previously
+ known upper time bound for this problem was $(Mkd)^{2^{O(n)}}$.",
+ paper = "Grig88.pdf"
+}
+
+\end{chunk}
+
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@inproceedings{Cann88,
+ author = "Canny, John",
+ title = "Some algebraic and geometric computations in PSPACE",
+ booktitle = "Proc 20th ACM Symp. on the theory of computing",
+ pages = "460-467",
+ year = "1988",
+ isbn = "0-89791-264-0",
+ link = "\url{http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-88-439.pdf}",
+ abstract =
+ "We give a PSPACE algorithm for determining the signs of multivariate
+ polynomials at the common zeros of a system of polynomial
+ equations. One of the consequences of this result is that the
+ ``Generalized Movers' Problem'' in robotics drops from EXPTIME into
+ PSPACE, and is therefore PSPACE-complete by a previous hardness result
+ [Rei]. We also show that the existential theory of the real numbers
+ can be decided in PSPACE. Other geometric problems that also drop into
+ PSPACE include the 3-d Euclidean Shortest Path Problem, and the ``2-d
+ Asteroid Avoidance Problem'' described in [RS]. Our method combines the
+ theorem of the primitive element from classical algebra with a
+ symbolic polynomial evaluation lemma from [BKR]. A decision problem
+ involving several algebraic numbers is reduced to a problem involving
+ a single algebraic number or primitive element, which rationally
+ generates all the given algebraic numbers.",
+ paper = "Cann88.pdf"
+}
+
+\end{chunk}
+
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@article{Cann93,
+ author = "Canny, John",
+ title = "Improved algorithms for sign and existential quantifier
+ elimination",
+ journal = "The Computer Journal",
+ volume = "36",
+ pages = "409-418",
+ year = "1993",
+ abstract =
+ "Recently there has been a lot of activity in algorithms that work
+ over real closed fields, and that perform such calculations as
+ quantifier elimination or computing connected components of
+ semi-algebraic sets. A cornerstone of this work is a symbolic sign
+ determination algorithm due to Ben-Or, Kozen and Reif. In this
+ paper we describe a new sign determination method based on the earlier
+ algorithm, but with two advantages: (i) It is faster in the univariate
+ case, and (ii) In the general case, it allows purely symbolic
+ quantifier elimination in pseudo-polynomial time. By purely symbolic,
+ we mean that it is possible to eliminate a quantified variable from a
+ system of polynomials no matter what the coefficient values are. The
+ previous methods required the coefficients to be themselves
+ polynomials in other variables. Our new method allows transcendental
+ functions or derivatives to appear in the coefficients.
+
+ Another corollary of the new sign-determination algorithm is a very
+ simple, practical algorithm for deciding existentially-quantified
+ formulae of the theory of the reals. We present an algorithm that has
+ a bit complexity of $n^{k+1}d^{O(k)}(c log n)^{1+\epsilon}$ randomized, or
+ $n^{n+1}d^{O(k^2)}c(1+\epsilon)$ deterministic, for any
+ $\epsilon>0$, where $n$ is the number
+ of polynomial constraints in the defining formula, $k$ is the number of
+ variables, $d$ is a bound on the degree, $c$ bounds the bit length of the
+ coefficient. The algorithm makes no general position assumptions, and
+ its constants are much smaller than other recent quantifier
+ elimination methods.",
+ paper = "Cann93.pdf"
+}
+
+\end{chunk}
+
+\index{Heintz, J.}
+\index{Roy, M-F.}
+\index{Solerno, P.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hein89,
+ author = "Heintz, J. and Roy, M-F. and Solerno, P.",
+ title = "On the complexity of semialgebraic sets",
+ booktitle = "Proc. IFIP",
+ pages = "293-298",
+ year = "1989"
+}
+
+\end{chunk}
+
+\index{Renegar, James}
+\begin{chunk}{axiom.bib}
+@article{Rene92,
+ author = "Renegar, James",
+ title = "On the computational complexity and geometry of the first-order
+ theory of the reals. Part I: Introduction"
+ journal = "J. of Symbolic Computation",
+ volume = "13",
+ number = "3",
+ year = "1992",
+ pages = "255-299",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717110800033}",
+ abstract =
+ "This series of papers presents a complete development and complexity
+ analysis of a decision method, and a quantifier elimination method,
+ for the first order theory of the reals. The complexity upper bounds
+ which are established are the best presently available, both for
+ sequential and parallel computation, and both for the bit model of
+ computation and the real number model of computation; except for the
+ bounds pertaining to the sequential decision method in the bit model
+ of computation, all bounds represent significant improvements over
+ previously established bounds.",
+ paper = "Rene92.pdf"
+}
+
+\end{chunk}
+
+\index{Renegar, James}
+\begin{chunk}{axiom.bib}
+@article{Rene92a,
+ author = "Renegar, James",
+ title = "On the computational complexity and geometry of the first-order
+ theory of the reals. Part II: The general decision problem"
+ journal = "J. of Symbolic Computation",
+ volume = "13",
+ number = "3",
+ year = "1992",
+ pages = "301-327",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717110800045}",
+ abstract =
+ "This series of papers presents a complete development and complexity
+ analysis of a decision method, and a quantifier elimination method,
+ for the first order theory of the reals. The complexity upper bounds
+ which are established are the best presently available, both for
+ sequential and parallel computation, and both for the bit model of
+ computation and the real number model of computation; except for the
+ bounds pertaining to the sequential decision method in the bit model
+ of computation, all bounds represent significant improvements over
+ previously established bounds.",
+ paper = "Rene92a.pdf"
+}
+
+\end{chunk}
+
+\index{Renegar, James}
+\begin{chunk}{axiom.bib}
+@article{Rene92b,
+ author = "Renegar, James",
+ title = "On the computational complexity and geometry of the first-order
+ theory of the reals. Part III: Quantifier elimination"
+ journal = "J. of Symbolic Computation",
+ volume = "13",
+ number = "3",
+ year = "1992",
+ pages = "329-352",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717110800057}",
+ abstract =
+ "This series of papers presents a complete development and complexity
+ analysis of a decision method, and a quantifier elimination method,
+ for the first order theory of the reals. The complexity upper bounds
+ which are established are the best presently available, both for
+ sequential and parallel computation, and both for the bit model of
+ computation and the real number model of computation; except for the
+ bounds pertaining to the sequential decision method in the bit model
+ of computation, all bounds represent significant improvements over
+ previously established bounds.",
+ paper = "Rene92b.pdf"
+}
+
+\end{chunk}
+
+\index{Arnon, Dennis S.}
+\begin{chunk}{axiom.bib}
+@article{Arno88c,
+ author = "Arnon, Dennis S.",
+ title = "A bibliography of quantifier elimination for real closed fields",
+ journal = "J. of Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ pages = "267-274",
+ year = "1988",
+ link =
+ "\url{http://www.sciencedirect.com/science/article/pii/S0747717188800166}",
+ abstract =
+ "A basic collection of literature relating to algorithmic quantifier
+ elimination for real closed fields is assembled",
+ paper = "Arno88c.pdf"
+}
+
+\end{chunk}
+
+\index{Seidenberg, A.}
+\begin{chunk}{axiom.bib}
+@article{Seid54,
+ author = "Seidenberg, A.",
+ title = "A New Decision Method for Elementary Algebra",
+ journal = "Annals of Mathematics",
+ volume = "60",
+ number = "2",
+ year = "1954",
+ pages = "365-374",
+ abstract =
+ "A. Tarski [4] has given a decision method for elementary algebra. In
+ essence this comes to giving an algorithm for deciding whether a
+ given finite set of polynomial inequalities has a solution. Below we
+ offer another proof of this result of Tarski. The main point of our
+ proof is accomplished upon showing how to decide whether a given
+ polynomial $f(x,y)$ in two variables, defined over the field \mathbb{R}
+ o rational numbers, has a zero in a real-closed field \mathbb{K}
+ containing $R^1$.
+ This is done in \S{}2, but for purposes of induction it is necessary to
+ consider also the case that the coefficients of $f(x,y)$ involve
+ parameters; the remarks in \S{}3 will be found sufficient for this
+ point. In \S{}1, the problem is reduced to a decision for equalities,
+ but an induction (on the number of unknowns) could not possibly be
+ carried out on equalities alone; we consider a simultaneous system
+ consisting of one equality $f(x,y) = 0$ and one inequality $F(x) \ne 0$.
+ Once the decision for this case is achieved, at least as in \S{}3,
+ the induction is immediate.",
+ paper = "Seid54.pdf"
+}
+
+\end{chunk}
+
+\index{Weispfenning, V.}
+\begin{chunk}{axiom.bib}
+@articl{Weis92,
+ author = "Weispfenning, V.",
+ title = "Comprehensive Groebner bases",
+ journal = "J. Symbolic Computation",
+ volume = "14",
+ number = "1",
+ year = "1992",
+ pages = "1-29",
+ abstract =
+ "Let $K$ be an integral domain and let $S$ be the polynomial ring
+ $K[U_1,\ldots,U_m; X_1,\ldots,X_n]$. For any finite $F \subseteq S$,
+ we construct a comprehensive Groebner basis of the ideal $Id(F)$, a
+ finite ideal basis of $Id(F)$ that is a Groebner basis of $Id(F)$
+ in $K^\prime[X_1,\ldots,X_n]$ for every specialization of the
+ parameters $U_1,\ldots,U_m$ in an arbitrary field $K^1$. We show
+ that this construction can be performed with the same worst case
+ degree bounds in the main variable $X_i$, as for ordinary Groebner
+ bases; moreover, examples computed in an ALDES/SAC-2 implementation
+ show that the construction is of practical value. Comprehensive
+ Groebner bases admit numerous applications to parametric problems
+ in algebraic geometry; in particular, they yield a fast elimination
+ of quantifier-blocks in algebraically closed fields",
+ paper = "Weis92.pdf"
+}
+
+\end{chunk}
+
+\index{Canny, John}
+\begin{chunk}{axiom.bib}
+@inproceeding{Cann87,
+ author = "Canny, John",
+ title = "A new algebraic method of robot motion planning and real geometry",
+ booktitle = "IEEE Symp. on Foundations of Comp. Sci.",
+ pages = "39-48",
+ abstract =
+ "We present an algorithm which solves the findpath or generalized
+ movers' problem in single exponential sequential time. This is the
+ first algorithm for the problem whose sequential time bound is less
+ than double exponential. In fact, the combinatorial exponent of the
+ algorithm is equal to the number of degrees of freedom, making it
+ worst-case optimal, and equaling or improving the time bounds of many
+ special purpose algorithms. The algorithm accepts a formula for a
+ semi-algebraic set S describing the set of free configurations and
+ produces a one-dimensional skeleton or ``roadmap'' of the set, which is
+ connected within each connected component of S. Additional points may
+ be linked to the roadmap in linear time. Our method draws from results
+ of singularity theory, and in particular makes use of the notion of
+ stratified sets as an efficient alternative to cell decomposition. We
+ introduce an algebraic tool called the multivariate resultant which
+ gives a necessary and sufficient condition for a system of homogeneous
+ polynomials to have a solution, and show that it can be computed in
+ polynomial parallel time. Among the consequences of this result are
+ new methods for quantifier elimination and an improved gap theorem for
+ the absolute value of roots of a system of polynomials.",
+ paper = "Cann87.pdf"
+}
+
+\end{chunk}
+
+\index{Pedersen, P.}
+\index{Roy, F.-F.}
+\index{Szpirglas, A.}
+\begin{chunk}{axiom.bib}
+@inproceeding{Pede93,
+ author = "Pedersen, P. and Roy, F.-F. and Szpirglas, A.",
+ title = "Counting real zeroes in the multivariate case",
+ booktitle = "Proc. MEGA'92: Computational Algebraic Geometry",
+ volume = "109",
+ pages = "203-224",
+ year = "1993",
+ abstract =
+ "In this paper we show, by generalizing Hermite’s theorem to the
+ multivariate setting, how to count the number of real or complex
+ points of a discrete algebraic set which lie within some algebraic
+ constraint region. We introduce a family of quadratic forms determined
+ by the algebraic constraints and defined in terms of the trace from
+ the coordinate ring of the variety to the ground field, and we show
+ that the rank and signature of these forms are sufficient to determine
+ the number of real points lying within a constraint region. In all
+ cases we count geometric points, which is to say, we count points
+ without multiplicity. The theoretical results on these quadratic forms
+ are more or less classical, but forgotten too, and can be found also
+ in [3].
+
+ We insist on effectivity of the computation and complexity analysis:
+ we show how to calculate the trace and signature using Gröbner bases,
+ and we show how the information provided by the individual quadratic
+ forms may be combined to determine the number of real points
+ satisfying a conjunction of constraints. The complexity of the
+ computation is polynomial in the dimension as a vector space of the
+ quotient ring associated to the defining equations. In terms of the
+ number of variables, the complexity of the computation is singly
+ exponential. The algorithm is well parallelizable.
+
+ We conclude the paper by applying our machinery to the problem of
+ effectively calculating the Euler characteristic of a smooth
+ hypersurface."
+}
+
+\end{chunk}
+
+\index{Weispfenning, V.}
+\begin{chunk}{axiom.bib}
+@articl{Weis88,
+ author = "Weispfenning, V.",
+ title = "The complexity of linear problems in fields",
+ journal = "J. of Symbolic Computation",
+ volume = "5",
+ number = "1-2",
+ year = "1988",
+ pages = "3-27",
+ link = "\url{http://www.sciencedirect.com.proxy.library.cmu.edu/science/article/pii/S0747717188800038}",
+ abstract =
+ "We consider linear problems in fields, ordered fields, discretely
+ valued fields (with finite residue field or residue field of
+ characteristic zero) and fields with finitely many independent
+ orderings and discrete valuations. Most of the fields considered will
+ be of characteristic zero. Formally, linear statements about these
+ structures (with parameters) are given by formulas of the respective
+ first-order language, in which all bound variables occur only
+ linearly. We study symbolic algorithms
+ ({\sl linear elimination procedures})
+ that reduce linear formulas to linear formulas of a very simple form,
+ i.e. quantifier-free linear formulas, and algorithms
+ ({\sl linear decision procedures})
+ that decide whether a given linear sentence holds in all
+ structures of the given class. For all classes of fields considered,
+ we find linear elimination procedures that run in double exponential
+ space and time. As a consequence, we can show that for fields (with
+ one or several discrete valuations), linear statements can be
+ transferred from characteristic zero to prime characteristic $p$,
+ provided $p$ is double exponential in the length of the statement. (For
+ similar bounds in the non-linear case, see Brown, 1978.) We find
+ corresponding linear decision procedures in the Berman complexity
+ classes $\bigcup_{c\in N} STA(*,2^{cn},dn)$
+ for $d = 1, 2$. In particular, all these procedures run in
+ exponential space. The technique employed is quantifier elimination
+ via Skolem terms based on Ferrante & Rackoff (1975). Using ideas of
+ Fischer & Rabin (1974), Berman (1977), Fürer (1982), we establish
+ lower bounds for these problems showing that our upper bounds are
+ essentially tight. For linear formulas with a bounded number of
+ quantifiers all our algorithms run in polynomial time. For linear
+ formulas of bounded quantifier alternation most of the algorithms run
+ in time $2^{O(n^k)} for fixed $k$.",
+ paper = "Weis88.pdf"
+}
+
+\end{chunk}
+
+\index{Weispfenning, V.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Weis94,
+ author = "Weispfenning, V.",
+ title = "Quantifier elimination for real algebra – the cubic case",
+ booktitle = "Proc ISSAC'94",
+ publisher = "ACM",
+ isbn = "0-89791-638-7",
+ pages = "258-263",
+ year = "1994",
+ abstract =
+ "We present a special purpose quantifier elimination method that
+ eliminates a quantifier $\exists x$ in formulas $\exists x(\rho)$
+ where $\rho$ is a boolean combination of polynomial inequalities of
+ degree $\le 3$ with respect to $x$. The method extends the virtual
+ substitition of parameterized test points developed in
+ [Weispfenning 1, Loos and Weispf.] for the linear case and in
+ [Weispfenning 2] for the quadratic case. It has similar upper
+ complexity bounds and offers similar advantages (relatively large
+ preprocessing part, explicit parametric solutions). Small examples
+ suggest that the method will be of practical significance.",
+ paper = "Weis94.pdf"
+}
+
+\end{chunk}
+
+\index{Loos, Rudiger}
+\index{Weispfenning, Volker}
+\begin{chunk}{axiom.bib}
+@article{Loos93,
+ author = "Loos, Rudiger and Weispfenning, Volker",
+ title = "Applying linear quantifier elimination",
+ journal = "The Computer Journal",
+ volume = "36",
+ number = "5",
+ year = "1993",
+ abstract =
+ "The linear quantifier elimination algorithm for ordered fields in
+ [15] is applicable to a wide range of examples involving even
+ non-linear parameters. The Skolem sets of the original algorithm
+ are generalized to elimination sets whose size is linear in the
+ number of atomic formulas, whereas the size of Skolem sets is
+ quadratic in this number. Elimiation sets may contain non-standard
+ terms which enter the computation symoblically. Many cases can be
+ treated by special methods improving further the empirical computing
+ times.",
+ paper = "Loos93.pdf"
+}
+
+\end{chunk}
+
+\index{Anai, Hirokazu}
+\index{Weispfenning, Volker}
+\begin{chunk}{axiom.bib}
+@inproceedings{Anai00,
+ author = "Anai, Hirokazu and d{Weispfenning, Volker",
+ title = "Deciding linear-trigonometric problems",
+ booktitle = "Proc ISSAC'00",
+ publisher = "ACM",
+ isbn = "1-58113-218-2",
+ year = "2000",
+ pages = "14-22",
+ abstract =
+ "In this paper, we present a decision procedure for certain
+ linear-trigonometric problems for the reals and integers formalized in
+ a suitable first-order language. The inputs are restricted to
+ formulas, where all but one of the quantified variables occur linearly
+ and at most one occurs both linearly and in a specific trigonometric
+ function. Moreover we may allow in addition the integer-part operation
+ in formulas. Besides ordinary quantifiers, we allow also counting
+ quantifiers. Furthermore we also determine the qualitative structure
+ of the connected components of the satisfaction set of the mixed
+ linear-trigonometric variable. We also consider the decision of these
+ problems in subfields of the real algebraic numbers.",
+ paper = "Anai00.pdf"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 8536c22..cd9ecf3 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5747,7 +5747,9 @@ bookvolbib reference for Cylindrical Algebraic Decomposition

20170528.01.tpd.patch
bookvolbib reference for Cylindrical Algebraic Decomposition

20170528.02.tpd.patch
-src/axiom-website/documentation.html Literate Programming talk
+src/axiom-website/documentation.html Literate Programming talk

+20170601.01.tpd.patch
+bookvolbib reference for Cylindrical Algebraic Decomposition

--
1.7.5.4