From 851069d7c2602ab8511f7dbf8e97fd90031e531e Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 7 Jun 2017 02:03:36 0400
Subject: [PATCH] bookvolbib reference for Cylindrical Algebraic Decomposition
MIMEVersion: 1.0
ContentType: text/plain; charset=UTF8
ContentTransferEncoding: 8bit
Goal: Axiom Algebra
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@inproceedings{Hong93,
author = "Hong, Hoon",
title = "Quantifier elimination for formulas constrained by
quadratic equations",
booktitle = "Proc. ISSAC'93",
year = "1993",
pages = "264274",
publisher = "ACM",
isbn = "0897916042",
abstract =
"An algorithm is given for constructing a quantifier free formula
(a boolean expression of polynomial equations and inequalitier)
equivalent to a given formula of the form:
$(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \and F]$, where $F$
is a quantifier free formula in $x_1,\ldots,x_r,x,$ and
$a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
coefficients such that the system
$\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
Formulas of this form frequently occur in the context of
constraint logic programming over the real numbers. The output
formulas are made of resultants and two variants, which we call
{\sl trace} and {\sl slope} resultants. Both of these variant
resultants can be expressed as determinants of certain matrices.",
paper = "Hong93.pdf"
}
\end{chunk}
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@article{Hong93a,
author = "Hong, Hoon",
title = "Quantifier Elimination for Formulas Constrained by
Quadratic Equations via Slope Resultants",
journal = "The Computer Journal",
volume = "36",
number = "5",
year = "1993",
pages = "439449",
abstract =
"An algorithm is given for eliminating the quantifier from a formula
$(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \and F]$, where $F$
is a quantifier free formula in $x_1,\ldots,x_r,x,$ and
$a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
coefficients such that the system
$\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
The output formulas are made of resultants and their variants,
which we call {\sl slope} resultants. The slope resultants can be,
like the resultants, expressed as determinants of certain matrices.
If we allow the determinant symbol in the output the computing time
of the algorithm is {\sl linear} in the length of the input. If not,
the computing time is dominated by $N(n^{2r+1}\ell+n^{2r}\ell^2)$
where $N$ is the number of polynomials in the input formula, $r$
is the number of variables, $n$ is the maximum of the degrees for
every variable, and $\ell$ is the maximum of the integer
coefficient bit lengths. Experimants with implementation suggest
that the algorithm is sufficiently efficient to be useful in practice.",
paper = "Hong93a.pdf"
}
\end{chunk}
\index{Hong, Hoon}
\index{El Din, Mohab Safey}
\begin{chunk}{axiom.bib}
@article{Hong12,
author = "Hong, Hoon and El Din, Mohab Safey",
title = "Variant Quantifier Elimination",
journal = "J. of Symbolic Computation",
volume = "47",
number = "7",
year = "2012",
pages = "883901",
abstract =
"We describe an algorithm (VQE) for a variant of the real quantifier
elimination problem (QE). The variant problem requires the input to
satisfy a certain {\sl extra condition},
and allows the output to be {\sl almost}
equivalent to the input. The motivation/rationale for studying such a
variant QE problem is that many quantified formulas arising in
applications do satisfy the extra conditions. Furthermore, in most
applications, it is sufficient that the output formula is almost
equivalent to the input formula. The main idea underlying the
algorithm is to substitute the repeated projection step of CAD by a
single projection without carrying out a parametric existential
decision over the reals. We find that the algorithm can tackle
important and challenging problems, such as numerical stability
analysis of the widelyused MacCormack’s scheme. The problem has been
practically out of reach for standard QE algorithms in spite of many
attempts to tackle it. However, the current implementation of VQE can
solve it in about 12 hours. This paper extends the results reported at
the conference ISSAC 2009.",
paper = "Hong12.pdf"
}
\end{chunk}
\index{Hong, Hoon}
\index{Sendra, J. Rafael}
\begin{chunk}{axiom.bib}
@inproceedings{Hong98a,
author = "Hong, Hoon and Sendra, J. Rafael",
title = "Computation of Variant Results",
booktitle = "Quantifier Elimination and Cylindrical Algebraic
Decomposition",
publisher = "Springer",
year = "1998",
isbn = "3211827943",
pages = "327337"
}
\end{chunk}
\index{Jovanovic, Dejan}
\index{de Moura, Leonardo}
\begin{chunk}{axiom.bib}
@misc{Jova12,
author = "Jovanovic, Dejan and de Moura, Leonardo",
title = "Solving NonLinear Arithmetic",
year = "2012",
link = "\url{http://cs.nyu.edu/~dejan/nonlinear/ijcar2012_extended.pdf}",
comment = "see: http://cs.nyu.edu/~dejan/nonlinear/",
abstract =
"We present a new algorithm for deciding satisfiability of nonlinear
arithmetic constraints. The algorithm performs a ConflictDriven
Clause Learning (CDCL) style search for a feasible assignment, while
using projection operators adapted from cylindrical algebraic
decomposition to guide the search away from the conflicting states.",
paper = "Jova12.pdf"
}
\end{chunk}
\index{England, Matthew}
\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@misc{Engl16,
author = "England, Matthew and Davenport, James H.",
title = "Experience with Heuristics, Benchmarks and Standards for
Cylindrical Algebraic Decomposition",
link = "\url{https://arxiv.org/pdf/1609.09269.pdf}",
abstract =
"n the paper which inspired the $SC^2$ project, [E. Abraham,
Building Bridges between Symbolic Computation and Satisfiability
Checking , Proc. ISSAC ’15, pp. 1–6, ACM, 2015] the author identified
the use of sophisticated heuristics as a technique that the
Satisfiability Checking community excels in and from which it is
likely the Symbolic Computation community could learn and prosper. To
start this learning process we summarise our experience with heuristic
development for the computer algebra algorithm Cylindrical Algebraic
Decomposition. We also propose and discuss standards and benchmarks as
another area where Symbolic Computation could prosper from
Satisfiability Checking expertise, noting that these have been
identified as initial actions for the new $SC^2$ community in the CSA
project, as described in [E.́ Abraham et al., SC 2 : {\sl Satisfiability
Checking meets Symbolic Computation (Project Paper)}, Intelligent
Computer Mathematics (LNCS 9761), pp. 28–43, Springer, 2015].",
paper = "Engl16.pdf"
}
\end{chunk}
\index{GonzalexVega, L.}
\begin{chunk}{axiom.bib}
@inproceedings{Gonz98,
author = "GonzalexVega, L.",
title = "A combinatorial algorithm solving some quantifier elimination
problems",
booktitle = "Quantifier Elimination and Cylindrical Algebraic
Decomposition",
isbn = "3211827943",
year = "1998",
pages = "365374",
}
\end{chunk}
\index{Gonzalex, Laureano}
\index{Henri, Lombardi}
\index{Recio, Tomas}
\index{Roy, MarieFrancoise}
\begin{chunk}{axiom.bib}
@inproceedings{Gonz89,
author = "Gonzalex, Laureano and Henri, Lombardi and Recio, Tomas and
Roy, MarieFrancoise",
title = "SturmHabicht sequence",
booktitle = "Proc. ACMSIGSAM 1989",
year = "1989",
pages = "136146",
isbn = "0897913256",
abstract =
"Formal computations with inequalities is a subject of general interest
in computer algebra. In particular it is fundamental in the
parallelisation of basic algorithms and quantifier elimination for real
closed filed ([BKR], [HRS]).
In $\S{}I$ we give a generalisation of Sturm theorem essentially due to
Sylvester which is the key for formal computations with inequalities.
Our result is an improvement of previously known results (see [BKR])
since no hypotheses have to be made on polynomials.
In $\S{}II$ we study the subresultant sequence. We precise some of the
classical definitions in order to avoid some problems appearing in the
paper by Loos ([L]) and study specialisation properties in detail.
In $\S{}III$ we introduce the SturmHabicht sequence, which generalises
Habicht's work ([H]). This new sequence obtained automatically from a
subresultant sequence has some remarkable properties:
\begin{itemize}
\item it gives the same information than the Sturm sequence, and this
information may be recovered by looking only at its principal
coefficients
\item it can be computed by ring operations and exact divisions only,
in polynomial time in case of integer coefficients, eventually by
modular methods
\item it has goos specialisation properties
\end{itemize}
Finally in $\S{}IV$ we give some information about applications and
implementation of the SturmHabicht sequence.",
paper = "Gonz89.pdf"
}
\end{chunk}
\index{Ratschan, Stefan}
\begin{chunk}{axiom.bib}
@article{Rats02,
author = "Ratschan, Stefan",
title = "Approximate quantified constraint solving by cylindrical box
decomposition",
year = "2002",
volume = "8",
number = "1",
pages = "2142",
abstract =
"This paper applies interval methods to a classical problem in
computer algebra. Let a quantified constraint be a firstorder formula
over the real numbers. As shown by A. Tarski in the 1930's, such
constraints, when restricted to the predicate symbols $<$, $=$ and
function symbols $+$, $\times$, are in general solvable.
However, the problem
becomes undecidable, when we add function symbols like
sin. Furthermore, all exact algorithms known up to now are too slow
for big examples, do not provide partial information before computing
the total result, cannot satisfactorily deal with interval constants
in the input, and often generate huge output. As a remedy we propose
an approximation method based on interval arithmetic. It uses a
generalization of the notion of cylindrical decomposition—as
introduced by G. Collins. We describe an implementation of the method
and demonstrate that, for quantified constraints without equalities,
it can efficiently give approximate information on problems that are
too hard for current exact methods."
}
\end{chunk}
\index{Hong, Hoon}
\index{Stahl, V.}
\begin{chunk}{axiom.bib}
@article{Hong94,
author = "Hong, Hoon and Stahl, V.",
title = "Safe start regions by fixed points and tightening",
journal = "Computing",
volume = "53",
number = "3",
pages = "323335",
abstract =
"In this paper, we present a method for finding safe starting regions
for a given system of nonlinear equations. The method is an
improvement of the usual method which is based on the fixed point
theorem. The improvement is obtained by enclosing the components of
the equation system by univariante interval polynomials whose zero
sets are found. This operation is called ``ightening''. Preliminary
experiments show that the tightening operation usually reduces the
number of bisections, and thus the computing time. The reduction seems
to become more dramatic when the number of variables increases."
}
\end{chunk}

books/bookvolbib.pamphlet  306 +++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  287 +++++++++++++++++++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 578 insertions(+), 19 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 2b0a9ee..688398e 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 8860,29 +8860,15 @@ Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael
reasoning in Aldor",
year = "1998",
link = "\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.1457}",
 abstract = "
 This paper examines the proposal of using the type system of Axiom to
+ abstract =
+ "This paper examines the proposal of using the type system of Axiom to
represent a logic, and thus to use the constructions of Axiom to
handle the logic and represent proofs and propositions, in the same
way as is done in theorem provers based on type theory such as Nuprl
or Coq.
The paper shows an interesting way to decorate Axiom with pre and
 postconditions.

 The CurryHoward correspondence used is
 \begin{tabular}{lcl}
 PROGRAMMING & & LOGIC\\
 Type & & Formula\\
 Program & & Proof\\
 Product/record type & (...,...) & Conjunction\\
 Sum/union type & \/ & Disjunction\\
 Function type & > & Implication\\
 Dependent function type & (x:A) > B(x) & Universal quantifier\\
 Dependent product type & (x:A,B(x)) & Existential quantifier\\
 Empty type & Exit & Contradictory proposition\\
 One element type & Triv & True proposition\\
 \end{tabular}",
+ postconditions.",
paper = "Poll98.pdf",
keywords = "axiomref"
}
@@ 15485,6 +15471,35 @@ Proc ISSAC 97 pp172175 (1997)
\subsection{E} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{England, Matthew}
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
+@misc{Engl16,
+ author = "England, Matthew and Davenport, James H.",
+ title = "Experience with Heuristics, Benchmarks and Standards for
+ Cylindrical Algebraic Decomposition",
+ link = "\url{https://arxiv.org/pdf/1609.09269.pdf}",
+ abstract =
+ "n the paper which inspired the $SC^2$ project, [E. Abraham,
+ Building Bridges between Symbolic Computation and Satisfiability
+ Checking , Proc. ISSAC ’15, pp. 1–6, ACM, 2015] the author identified
+ the use of sophisticated heuristics as a technique that the
+ Satisfiability Checking community excels in and from which it is
+ likely the Symbolic Computation community could learn and prosper. To
+ start this learning process we summarise our experience with heuristic
+ development for the computer algebra algorithm Cylindrical Algebraic
+ Decomposition. We also propose and discuss standards and benchmarks as
+ another area where Symbolic Computation could prosper from
+ Satisfiability Checking expertise, noting that these have been
+ identified as initial actions for the new $SC^2$ community in the CSA
+ project, as described in [E.́ Abraham et al., SC 2 : {\sl Satisfiability
+ Checking meets Symbolic Computation (Project Paper)}, Intelligent
+ Computer Mathematics (LNCS 9761), pp. 28–43, Springer, 2015].",
+ paper = "Engl16.pdf"
+}
+
+\end{chunk}
+
\index{RealClosure}
\index{Emiris, Ioannis Z.}
\index{Tsigaridas, Elias P.}
@@ 15672,6 +15687,69 @@ Proc ISSAC 97 pp172175 (1997)
\subsection{G} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Gonzalex, Laureano}
+\index{Henri, Lombardi}
+\index{Recio, Tomas}
+\index{Roy, MarieFrancoise}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gonz89,
+ author = "Gonzalex, Laureano and Henri, Lombardi and Recio, Tomas and
+ Roy, MarieFrancoise",
+ title = "SturmHabicht sequence",
+ booktitle = "Proc. ACMSIGSAM 1989",
+ year = "1989",
+ pages = "136146",
+ isbn = "0897913256",
+ abstract =
+ "Formal computations with inequalities is a subject of general interest
+ in computer algebra. In particular it is fundamental in the
+ parallelisation of basic algorithms and quantifier elimination for real
+ closed filed ([BKR], [HRS]).
+
+ In $\S{}I$ we give a generalisation of Sturm theorem essentially due to
+ Sylvester which is the key for formal computations with inequalities.
+ Our result is an improvement of previously known results (see [BKR])
+ since no hypotheses have to be made on polynomials.
+
+ In $\S{}II$ we study the subresultant sequence. We precise some of the
+ classical definitions in order to avoid some problems appearing in the
+ paper by Loos ([L]) and study specialisation properties in detail.
+
+ In $\S{}III$ we introduce the SturmHabicht sequence, which generalises
+ Habicht's work ([H]). This new sequence obtained automatically from a
+ subresultant sequence has some remarkable properties:
+ \begin{itemize}
+ \item it gives the same information than the Sturm sequence, and this
+ information may be recovered by looking only at its principal
+ coefficients
+ \item it can be computed by ring operations and exact divisions only,
+ in polynomial time in case of integer coefficients, eventually by
+ modular methods
+ \item it has goos specialisation properties
+ \end{itemize}
+
+ Finally in $\S{}IV$ we give some information about applications and
+ implementation of the SturmHabicht sequence.",
+ paper = "Gonz89.pdf"
+}
+
+\end{chunk}
+
+\index{GonzalexVega, L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gonz98,
+ author = "GonzalexVega, L.",
+ title = "A combinatorial algorithm solving some quantifier elimination
+ problems",
+ booktitle = "Quantifier Elimination and Cylindrical Algebraic
+ Decomposition",
+ isbn = "3211827943",
+ year = "1998",
+ pages = "365374",
+}
+
+\end{chunk}
+
\index{Grigor'ev, D. Yu.}
\index{Vorobjov, N. N.}
\begin{chunk}{axiom.bib}
@@ 15812,6 +15890,95 @@ Proc ISSAC 97 pp172175 (1997)
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
+@inproceedings{Hong93,
+ author = "Hong, Hoon",
+ title = "Quantifier elimination for formulas constrained by
+ quadratic equations",
+ booktitle = "Proc. ISSAC'93",
+ year = "1993",
+ pages = "264274",
+ publisher = "ACM",
+ isbn = "0897916042",
+ abstract =
+ "An algorithm is given for constructing a quantifier free formula
+ (a boolean expression of polynomial equations and inequalitier)
+ equivalent to a given formula of the form:
+ $(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \land F]$, where $F$
+ is a quantifier free formula in $x_1,\ldots,x_r,x,$ and
+ $a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
+ coefficients such that the system
+ $\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
+ Formulas of this form frequently occur in the context of
+ constraint logic programming over the real numbers. The output
+ formulas are made of resultants and two variants, which we call
+ {\sl trace} and {\sl slope} resultants. Both of these variant
+ resultants can be expressed as determinants of certain matrices.",
+ paper = "Hong93.pdf"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
+@article{Hong93a,
+ author = "Hong, Hoon",
+ title = "Quantifier Elimination for Formulas Constrained by
+ Quadratic Equations via Slope Resultants",
+ journal = "The Computer Journal",
+ volume = "36",
+ number = "5",
+ year = "1993",
+ pages = "439449",
+ abstract =
+ "
+ An algorithm is given for eliminating the quantifier from a formula
+ $(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \land F]$, where $F$
+ is a quantifier free formula in $x_1,\ldots,x_r,x$ and
+ $a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
+ coefficients such that the system
+ $\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
+ The output formulas are made of resultants and their variants,
+ which we call {\sl slope} resultants. The slope resultants can be,
+ like the resultants, expressed as determinants of certain matrices.
+ If we allow the determinant symbol in the output the computing time
+ of the algorithm is {\sl linear} in the length of the input. If not,
+ the computing time is dominated by $N(n^{2r+1}\ell+n^{2r}\ell^2)$
+ where $N$ is the number of polynomials in the input formula, $r$
+ is the number of variables, $n$ is the maximum of the degrees for
+ every variable, and $\ell$ is the maximum of the integer
+ coefficient bit lengths. Experimants with implementation suggest
+ that the algorithm is sufficiently efficient to be useful in practice.",
+ paper = "Hong93a.pdf"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\index{Stahl, V.}
+\begin{chunk}{axiom.bib}
+@article{Hong94,
+ author = "Hong, Hoon and Stahl, V.",
+ title = "Safe start regions by fixed points and tightening",
+ journal = "Computing",
+ volume = "53",
+ number = "3",
+ pages = "323335",
+ abstract =
+ "In this paper, we present a method for finding safe starting regions
+ for a given system of nonlinear equations. The method is an
+ improvement of the usual method which is based on the fixed point
+ theorem. The improvement is obtained by enclosing the components of
+ the equation system by univariante interval polynomials whose zero
+ sets are found. This operation is called ``ightening''. Preliminary
+ experiments show that the tightening operation usually reduces the
+ number of bisections, and thus the computing time. The reduction seems
+ to become more dramatic when the number of variables increases."
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
@inproceedings{Hong98,
author = "Hong, Hoon",
title = "Simple Solution Formula Construction in Cylindrical
@@ 15845,6 +16012,22 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
\index{Hong, Hoon}
+\index{Sendra, J. Rafael}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hong98a,
+ author = "Hong, Hoon and Sendra, J. Rafael",
+ title = "Computation of Variant Results",
+ booktitle = "Quantifier Elimination and Cylindrical Algebraic
+ Decomposition",
+ publisher = "Springer",
+ year = "1998",
+ isbn = "3211827943",
+ pages = "327337"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@misc{Hong05,
author = "Hong, Hoon",
@@ 15855,6 +16038,63 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Hong, Hoon}
+\index{El Din, Mohab Safey}
+\begin{chunk}{axiom.bib}
+@article{Hong12,
+
+ title = "Variant Quantifier Elimination",
+ journal = "J. of Symbolic Computation",
+ volume = "47",
+ number = "7",
+ year = "2012",
+ pages = "883901",
+ abstract =
+ "We describe an algorithm (VQE) for a variant of the real quantifier
+ elimination problem (QE). The variant problem requires the input to
+ satisfy a certain {\sl extra condition},
+ and allows the output to be {\sl almost}
+ equivalent to the input. The motivation/rationale for studying such a
+ variant QE problem is that many quantified formulas arising in
+ applications do satisfy the extra conditions. Furthermore, in most
+ applications, it is sufficient that the output formula is almost
+ equivalent to the input formula. The main idea underlying the
+ algorithm is to substitute the repeated projection step of CAD by a
+ single projection without carrying out a parametric existential
+ decision over the reals. We find that the algorithm can tackle
+ important and challenging problems, such as numerical stability
+ analysis of the widelyused MacCormack’s scheme. The problem has been
+ practically out of reach for standard QE algorithms in spite of many
+ attempts to tackle it. However, the current implementation of VQE can
+ solve it in about 12 hours. This paper extends the results reported at
+ the conference ISSAC 2009.",
+ paper = "Hong12.pdf"
+}
+
+\end{chunk}
+
+\subsection{J} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Jovanovic, Dejan}
+\index{de Moura, Leonardo}
+\begin{chunk}{axiom.bib}
+@misc{Jova12,
+ author = "Jovanovic, Dejan and de Moura, Leonardo",
+ title = "Solving NonLinear Arithmetic",
+ year = "2012",
+ link = "\url{http://cs.nyu.edu/~dejan/nonlinear/ijcar2012_extended.pdf}",
+ comment = "see: http://cs.nyu.edu/~dejan/nonlinear/",
+ abstract =
+ "We present a new algorithm for deciding satisfiability of nonlinear
+ arithmetic constraints. The algorithm performs a ConflictDriven
+ Clause Learning (CDCL) style search for a feasible assignment, while
+ using projection operators adapted from cylindrical algebraic
+ decomposition to guide the search away from the conflicting states.",
+ paper = "Jova12.pdf"
+}
+
+\end{chunk}
+
\subsection{L} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{LaValle, Steven M.}
@@ 16095,6 +16335,38 @@ Proc ISSAC 97 pp172175 (1997)
\subsection{R} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\index{Ratschan, Stefan}
+\begin{chunk}{axiom.bib}
+@article{Rats02,
+ author = "Ratschan, Stefan",
+ title = "Approximate quantified constraint solving by cylindrical box
+ decomposition",
+ year = "2002",
+ volume = "8",
+ number = "1",
+ pages = "2142",
+ abstract =
+ "This paper applies interval methods to a classical problem in
+ computer algebra. Let a quantified constraint be a firstorder formula
+ over the real numbers. As shown by A. Tarski in the 1930's, such
+ constraints, when restricted to the predicate symbols $<$, $=$ and
+ function symbols $+$, $\times$, are in general solvable.
+ However, the problem
+ becomes undecidable, when we add function symbols like
+ sin. Furthermore, all exact algorithms known up to now are too slow
+ for big examples, do not provide partial information before computing
+ the total result, cannot satisfactorily deal with interval constants
+ in the input, and often generate huge output. As a remedy we propose
+ an approximation method based on interval arithmetic. It uses a
+ generalization of the notion of cylindrical decomposition—as
+ introduced by G. Collins. We describe an implementation of the method
+ and demonstrate that, for quantified constraints without equalities,
+ it can efficiently give approximate information on problems that are
+ too hard for current exact methods."
+}
+
+\end{chunk}
+
\index{Renegar, James}
\begin{chunk}{axiom.bib}
@article{Rene92,
diff git a/changelog b/changelog
index 1d5160f..8039eb1 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170607 tpd src/axiomwebsite/patches.html 20170607.01.tpd.patch
+20170607 tpd bookvolbib reference for Cylindrical Algebraic Decomposition
20170602 tpd src/axiomwebsite/patches.html 20170602.01.tpd.patch
20170602 kyk bookvol13 Keshav Kini  fix typos
20170602 kyk bookvol14 Keshav Kini  fix typos
diff git a/patch b/patch
index 9b3c1d9..6ffd26b 100644
 a/patch
+++ b/patch
@@ 1,3 +1,286 @@
bookvol13 Keshav Kini  fix typos
+bookvolbib reference for Cylindrical Algebraic Decomposition
Goal: Axiom Maintenance
+Goal: Axiom Algebra
+
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hong93,
+ author = "Hong, Hoon",
+ title = "Quantifier elimination for formulas constrained by
+ quadratic equations",
+ booktitle = "Proc. ISSAC'93",
+ year = "1993",
+ pages = "264274",
+ publisher = "ACM",
+ isbn = "0897916042",
+ abstract =
+ "An algorithm is given for constructing a quantifier free formula
+ (a boolean expression of polynomial equations and inequalitier)
+ equivalent to a given formula of the form:
+ $(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \and F]$, where $F$
+ is a quantifier free formula in $x_1,\ldots,x_r,x,$ and
+ $a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
+ coefficients such that the system
+ $\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
+ Formulas of this form frequently occur in the context of
+ constraint logic programming over the real numbers. The output
+ formulas are made of resultants and two variants, which we call
+ {\sl trace} and {\sl slope} resultants. Both of these variant
+ resultants can be expressed as determinants of certain matrices.",
+ paper = "Hong93.pdf"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
+@article{Hong93a,
+ author = "Hong, Hoon",
+ title = "Quantifier Elimination for Formulas Constrained by
+ Quadratic Equations via Slope Resultants",
+ journal = "The Computer Journal",
+ volume = "36",
+ number = "5",
+ year = "1993",
+ pages = "439449",
+ abstract =
+ "An algorithm is given for eliminating the quantifier from a formula
+ $(\exists x \in \mathbb{R})[a_x^2+a_1x+a_0=0 \and F]$, where $F$
+ is a quantifier free formula in $x_1,\ldots,x_r,x,$ and
+ $a_2,a_1,a_0$ are polynomials in $x_1,\ldots,x_r$ with real
+ coefficients such that the system
+ $\{a_2=0,a_1=0,a_0=0\}$ has no solution in $\mathbb{R}^r$.
+ The output formulas are made of resultants and their variants,
+ which we call {\sl slope} resultants. The slope resultants can be,
+ like the resultants, expressed as determinants of certain matrices.
+ If we allow the determinant symbol in the output the computing time
+ of the algorithm is {\sl linear} in the length of the input. If not,
+ the computing time is dominated by $N(n^{2r+1}\ell+n^{2r}\ell^2)$
+ where $N$ is the number of polynomials in the input formula, $r$
+ is the number of variables, $n$ is the maximum of the degrees for
+ every variable, and $\ell$ is the maximum of the integer
+ coefficient bit lengths. Experimants with implementation suggest
+ that the algorithm is sufficiently efficient to be useful in practice.",
+ paper = "Hong93a.pdf"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\index{El Din, Mohab Safey}
+\begin{chunk}{axiom.bib}
+@article{Hong12,
+ author = "Hong, Hoon and El Din, Mohab Safey",
+ title = "Variant Quantifier Elimination",
+ journal = "J. of Symbolic Computation",
+ volume = "47",
+ number = "7",
+ year = "2012",
+ pages = "883901",
+ abstract =
+ "We describe an algorithm (VQE) for a variant of the real quantifier
+ elimination problem (QE). The variant problem requires the input to
+ satisfy a certain {\sl extra condition},
+ and allows the output to be {\sl almost}
+ equivalent to the input. The motivation/rationale for studying such a
+ variant QE problem is that many quantified formulas arising in
+ applications do satisfy the extra conditions. Furthermore, in most
+ applications, it is sufficient that the output formula is almost
+ equivalent to the input formula. The main idea underlying the
+ algorithm is to substitute the repeated projection step of CAD by a
+ single projection without carrying out a parametric existential
+ decision over the reals. We find that the algorithm can tackle
+ important and challenging problems, such as numerical stability
+ analysis of the widelyused MacCormack’s scheme. The problem has been
+ practically out of reach for standard QE algorithms in spite of many
+ attempts to tackle it. However, the current implementation of VQE can
+ solve it in about 12 hours. This paper extends the results reported at
+ the conference ISSAC 2009.",
+ paper = "Hong12.pdf"
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\index{Sendra, J. Rafael}
+\begin{chunk}{axiom.bib}
+@inproceedings{Hong98a,
+ author = "Hong, Hoon and Sendra, J. Rafael",
+ title = "Computation of Variant Results",
+ booktitle = "Quantifier Elimination and Cylindrical Algebraic
+ Decomposition",
+ publisher = "Springer",
+ year = "1998",
+ isbn = "3211827943",
+ pages = "327337"
+}
+
+\end{chunk}
+
+\index{Jovanovic, Dejan}
+\index{de Moura, Leonardo}
+\begin{chunk}{axiom.bib}
+@misc{Jova12,
+ author = "Jovanovic, Dejan and de Moura, Leonardo",
+ title = "Solving NonLinear Arithmetic",
+ year = "2012",
+ link = "\url{http://cs.nyu.edu/~dejan/nonlinear/ijcar2012_extended.pdf}",
+ comment = "see: http://cs.nyu.edu/~dejan/nonlinear/",
+ abstract =
+ "We present a new algorithm for deciding satisfiability of nonlinear
+ arithmetic constraints. The algorithm performs a ConflictDriven
+ Clause Learning (CDCL) style search for a feasible assignment, while
+ using projection operators adapted from cylindrical algebraic
+ decomposition to guide the search away from the conflicting states.",
+ paper = "Jova12.pdf"
+}
+
+\end{chunk}
+
+\index{England, Matthew}
+\index{Davenport, James H.}
+\begin{chunk}{axiom.bib}
+@misc{Engl16,
+ author = "England, Matthew and Davenport, James H.",
+ title = "Experience with Heuristics, Benchmarks and Standards for
+ Cylindrical Algebraic Decomposition",
+ link = "\url{https://arxiv.org/pdf/1609.09269.pdf}",
+ abstract =
+ "n the paper which inspired the $SC^2$ project, [E. Abraham,
+ Building Bridges between Symbolic Computation and Satisfiability
+ Checking , Proc. ISSAC ’15, pp. 1–6, ACM, 2015] the author identified
+ the use of sophisticated heuristics as a technique that the
+ Satisfiability Checking community excels in and from which it is
+ likely the Symbolic Computation community could learn and prosper. To
+ start this learning process we summarise our experience with heuristic
+ development for the computer algebra algorithm Cylindrical Algebraic
+ Decomposition. We also propose and discuss standards and benchmarks as
+ another area where Symbolic Computation could prosper from
+ Satisfiability Checking expertise, noting that these have been
+ identified as initial actions for the new $SC^2$ community in the CSA
+ project, as described in [E.́ Abraham et al., SC 2 : {\sl Satisfiability
+ Checking meets Symbolic Computation (Project Paper)}, Intelligent
+ Computer Mathematics (LNCS 9761), pp. 28–43, Springer, 2015].",
+ paper = "Engl16.pdf"
+}
+
+\end{chunk}
+
+\index{GonzalexVega, L.}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gonz98,
+ author = "GonzalexVega, L.",
+ title = "A combinatorial algorithm solving some quantifier elimination
+ problems",
+ booktitle = "Quantifier Elimination and Cylindrical Algebraic
+ Decomposition",
+ isbn = "3211827943",
+ year = "1998",
+ pages = "365374",
+}
+
+\end{chunk}
+
+\index{Gonzalex, Laureano}
+\index{Henri, Lombardi}
+\index{Recio, Tomas}
+\index{Roy, MarieFrancoise}
+\begin{chunk}{axiom.bib}
+@inproceedings{Gonz89,
+ author = "Gonzalex, Laureano and Henri, Lombardi and Recio, Tomas and
+ Roy, MarieFrancoise",
+ title = "SturmHabicht sequence",
+ booktitle = "Proc. ACMSIGSAM 1989",
+ year = "1989",
+ pages = "136146",
+ isbn = "0897913256",
+ abstract =
+ "Formal computations with inequalities is a subject of general interest
+ in computer algebra. In particular it is fundamental in the
+ parallelisation of basic algorithms and quantifier elimination for real
+ closed filed ([BKR], [HRS]).
+
+ In $\S{}I$ we give a generalisation of Sturm theorem essentially due to
+ Sylvester which is the key for formal computations with inequalities.
+ Our result is an improvement of previously known results (see [BKR])
+ since no hypotheses have to be made on polynomials.
+
+ In $\S{}II$ we study the subresultant sequence. We precise some of the
+ classical definitions in order to avoid some problems appearing in the
+ paper by Loos ([L]) and study specialisation properties in detail.
+
+ In $\S{}III$ we introduce the SturmHabicht sequence, which generalises
+ Habicht's work ([H]). This new sequence obtained automatically from a
+ subresultant sequence has some remarkable properties:
+ \begin{itemize}
+ \item it gives the same information than the Sturm sequence, and this
+ information may be recovered by looking only at its principal
+ coefficients
+ \item it can be computed by ring operations and exact divisions only,
+ in polynomial time in case of integer coefficients, eventually by
+ modular methods
+ \item it has goos specialisation properties
+ \end{itemize}
+
+ Finally in $\S{}IV$ we give some information about applications and
+ implementation of the SturmHabicht sequence.",
+ paper = "Gonz89.pdf"
+}
+
+\end{chunk}
+
+\index{Ratschan, Stefan}
+\begin{chunk}{axiom.bib}
+@article{Rats02,
+ author = "Ratschan, Stefan",
+ title = "Approximate quantified constraint solving by cylindrical box
+ decomposition",
+ year = "2002",
+ volume = "8",
+ number = "1",
+ pages = "2142",
+ abstract =
+ "This paper applies interval methods to a classical problem in
+ computer algebra. Let a quantified constraint be a firstorder formula
+ over the real numbers. As shown by A. Tarski in the 1930's, such
+ constraints, when restricted to the predicate symbols $<$, $=$ and
+ function symbols $+$, $\times$, are in general solvable.
+ However, the problem
+ becomes undecidable, when we add function symbols like
+ sin. Furthermore, all exact algorithms known up to now are too slow
+ for big examples, do not provide partial information before computing
+ the total result, cannot satisfactorily deal with interval constants
+ in the input, and often generate huge output. As a remedy we propose
+ an approximation method based on interval arithmetic. It uses a
+ generalization of the notion of cylindrical decomposition—as
+ introduced by G. Collins. We describe an implementation of the method
+ and demonstrate that, for quantified constraints without equalities,
+ it can efficiently give approximate information on problems that are
+ too hard for current exact methods."
+}
+
+\end{chunk}
+
+\index{Hong, Hoon}
+\index{Stahl, V.}
+\begin{chunk}{axiom.bib}
+@article{Hong94,
+ author = "Hong, Hoon and Stahl, V.",
+ title = "Safe start regions by fixed points and tightening",
+ journal = "Computing",
+ volume = "53",
+ number = "3",
+ pages = "323335",
+ abstract =
+ "In this paper, we present a method for finding safe starting regions
+ for a given system of nonlinear equations. The method is an
+ improvement of the usual method which is based on the fixed point
+ theorem. The improvement is obtained by enclosing the components of
+ the equation system by univariante interval polynomials whose zero
+ sets are found. This operation is called ``ightening''. Preliminary
+ experiments show that the tightening operation usually reduces the
+ number of bisections, and thus the computing time. The reduction seems
+ to become more dramatic when the number of variables increases."
+}
+
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 731a0ec..eb24f25 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5752,6 +5752,8 @@ src/axiomwebsite/documentation.html Literate Programming talk
bookvolbib reference for Cylindrical Algebraic Decomposition
20170602.01.tpd.patch
bookvol13 Keshav Kini  fix typos
+20170607.01.tpd.patch
+bookvolbib reference for Cylindrical Algebraic Decomposition

1.7.5.4