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