From ec5a09897f479801283262d1eac212b32974236f Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sat, 27 May 2017 14:35:56 0400
Subject: [PATCH] bookvolbib reference for Cylindrical Algebraic Decomposition
Goal: Axiom Algebra
\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@misc{Hong05,
author = "Hong, Hoon",
title = "Tutorial on CAD",
year = "2005",
paper = "Hong05.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  206 +++++++++++++++++++++++++++++
changelog  4 +
patch  269 ++
src/axiomwebsite/patches.html  4 +
4 files changed, 216 insertions(+), 267 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 65e830c..ce8dbdb 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 5853,6 +5853,40 @@ Martin, U.
\subsection{B} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Ballarin, Clemens}
+\index{Homann, Karsten}
+\index{Calmet, Jacques}
+\begin{chunk}{axiom.bib}
+@inproceedings{Ball95,
+ author = "Ballarin, Clemens and Homann, Karsten and Calmet, Jacques",
+ title = "Theorems and Algorithms: An Interface between Isabelle and Maple",
+ booktitle = "ISSAC 95",
+ year = "1995",
+ pages = "150157",
+ publisher = "ACM",
+ link = "\url{https://pdfs.semanticscholar.org/077e/606f92b4095637e624a9efc942c5c63c4bc2.pdf}",
+ abstract =
+ "Solving sophisticated mathematical problems often requires algebraic
+ algorithms {\sl and} theorems. However, there are no environments
+ integrating theorem provers and computer algebra systems which
+ consistently provide the inference capabilities of the first and the
+ powerful arithmetic of the latter systems.
+
+ As an example for such a mechanized mathematics environment we describe
+ a prototype implementation of an interface between Isabelle and Maple.
+ It is achieved by extending the simplifier of Isabelle through the
+ introduction of a new class of simplification rules called evaluation
+ rules in order to make selected operations of Maple available, and
+ without any modification to the computer algebra system. Additionally,
+ we specify syntax translations for the concrete syntax of Maple
+ which enables the communication between both systems illustrated by
+ some examples that can be solved by theorems and algorithms",
+ paper = "Ball95.pdf"
+
+}
+
+\end{chunk}
+
+\index{Ballarin, Clemens}
\index{Paulson, Lawrence C.}
\begin{chunk}{axiom.bib}
@misc{Ball98,
@@ 5918,6 +5952,52 @@ Martin, U.
\end{chunk}
+\index{Barendregt, Henk}
+\index{Cohen, Arjeh M.}
+\begin{chunk}{axiom.bib}
+@article{Bare01,
+ author = "Barendregt, Henk and Cohen, Arjeh M.",
+ title = "Electronic Communication of Mathematics and the Interaction
+ of Computer Algebra Systems and Proof Assistants",
+ journal = "J. Symbolic Computation",
+ volume = "32",
+ pages = "322",
+ year = "2001",
+ abstract =
+ "Present day computer algebra systems (CASs) and proof assistants
+ (PAs) are specialized programs that help humans with mathematical
+ computations and deductions. Although several such systems are
+ impressive, they all have certain limitations. In most CASs side
+ conditions that are essential for the truth of an equality are not
+ formulated; moreover there are bugs. The PAs have a limited power for
+ computing and hence also for assistance with proofs. Almost all
+ examples of both categories are stand alone special purpose systems
+ and therefore they cannot communicate with each other.
+
+ We will argue that the present state of the art in logic is such that
+ there is a natural formal language, independent of the special purpose
+ application in question, by which these systems can communicate
+ mathematical statements. In this way their individual power will be
+ enhanced.
+
+ Statements received at one particular location from other sites fall
+ into two categories: with or without the qualification ``evidently
+ impeccable'', a notion that is methodologi cally precise and
+ sound. For statements having this quality assessment the evidence may
+ come from the other site or from the local site itself, but in both
+ cases it is verified locally. In cases where there is no evidence of
+ impeccability one has to rely on cross checking. There is a tradeoff
+ between these two kinds of statements: for impeccability one has to
+ pay the price of obtaining less power.
+
+ Some examples of communication forms are given that show how the
+ participants benefit",
+ paper = "Bare01.pdf"
+}
+
+\end{chunk}
+
+
\index{Bauer, Andrej}
\begin{chunk}{axiom.bib}
@article{Baue16,
@@ 6237,6 +6317,57 @@ Martin, U.
\end{chunk}
+\index{Boulton, Richard John}
+\begin{chunk}{axiom.bib}
+@techreport{Boul94,
+ author = "Boulton, Richard John",
+ title = "Efficiency in a fullyexpansive Theorem Prover",
+ year = "1994",
+ type = "technical report",
+ number = "UCAMCLTR337",
+ institution = "University of Cambridge",
+ abstract =
+ "The HOL system is a fullyexpansive theorem prover: Proofs generated
+ in the system are composed of applications of the primitive inference
+ rules of the underlying logic. This has two main advantages. First,
+ the soundness of the system depends only on the implementations of the
+ primitive rules. Second, users can be given the freedom to write their
+ own proof procedures without the risk of making the system unsound. A
+ full functional programming language is provided for this purpose. The
+ disadvantage with the approach is that performance is
+ compromised. This is partly due to the inherent cost of fully
+ expanding a proof but, as demonstrated in this thesis, much of the
+ observed inefficiency is due to the way the derived proof procedures
+ are written. This thesis seeks to identify sources of noninherent
+ inefficiency in the HOL system and proposes some generalpurpose and
+ some specialised techniques for eliminating it. One area that seems to
+ be particularly amenable to optimisation is equational reasoning. This
+ is significant because equational reasoning constitutes large portions
+ of many proofs. A number of techniques are proposed that transparently
+ optimise equational reasoning. Existing programs in the HOL system
+ require little or no modification to work faster. The other major
+ contribution of this thesis is a framework in which part of the
+ computation involved in HOL proofs can be postponed. This enables
+ users to make better use of their time. The technique exploits a form
+ of lazy evaluation. The critical feature is the separation of the code
+ that generates the structure of a theorem from the code that justifies
+ it logically. Delaying the justification allows some nonlocal
+ optimisations to be performed in equational reasoning. None of the
+ techniques sacrifice the security of the fullyexpansive approach. A
+ decision procedure for a subset of the theory of linear arithmetic is
+ used to illustrate many of the techniques. Decision procedures for
+ this theory are commonplace in theorem provers due to the importance
+ of arithmetic reasoning. The techniques described in the thesis have
+ been implemented and execution times are given. The implementation of
+ the arithmetic procedure is a major contribution in itself. For the
+ first time, users of the HOL system are able to prove many arithmetic
+ lemmas automatically in a practical amount of time (typically a second
+ or two). The applicability of the techniques to other fullyexpansive
+ theorem provers and possile extensions of the ideas are considered."
+}
+
+\end{chunk}
+
\index{Bove, Ana}
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@@ 6492,6 +6623,19 @@ Martin, U.
\end{chunk}
+\index{Clarke, Edmund}
+\index{Zhao, Xudong}
+\begin{chunk}{axiom.bib}
+@misc{Clar91,
+ author = "Clarke, Edmund and Zhao, Xudong",
+ title = "Analytica  A Theorem Prover in Mathematica",
+ year = "1991",
+ link = "\url{http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Analytica%20A%20Theorem%20Prover%20in%20Mathematica.pdf}",
+ paper = "Clar91.pdf"
+}
+
+\end{chunk}
+
\index{Comon, H.}
\index{Lugiez, D.}
\index{Schnoebelen, P.H.}
@@ 6866,10 +7010,16 @@ England, Matthew; Wilson, David
\index{Dos Reis, Gabriel}
\index{Matthews, David}
\index{Li, Yue}
\begin{chunk}{ignore}
\bibitem[Dos Reis 11]{DR11} Dos Reis, Gabriel; Matthews, David; Li, Yue
 title = "Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework",
Calculemus (2011) Springer
+\begin{chunk}{axiom.bib}
+@inbook{Dosr11,
+ author = "Dos Reis, Gabriel and Matthews, David and Li, Yue",
+ title = "Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof
+ Assistants and Computer Algebra System Framework",
+ booktitle = "Calculemus",
+ pages = "1529",
+ year = "2011",
+ publisher = "Springer",
+ isbn = "9783642226731",
link = "\url{http://paradise.caltech.edu/~yli/paper/oapolyml.pdf}",
abstract = "
This paper presents an ongoing effort to integrate the Axiom family of
@@ 6880,8 +7030,9 @@ Calculemus (2011) Springer
verification to a family of strongly typed computer algebra systems at
a modest cost. Our approach is based on retargeting the code generator
of the OpenAxiom compiler to the Poly/ML abstract machine.",
 paper = "DR11.pdf",
+ paper = "Dosr11.pdf",
keywords = "axiomref"
+}
\end{chunk}
@@ 7613,6 +7764,35 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Komendantsky, Vladimir}
+\index{Konovalov, Alexander}
+\index{Linton, Steve}
+\begin{chunk}{axiom.bib}
+@article{Kome11,
+ author = "Komendantsky, Vladimir and Konovalov, Alexander and Linton, Steve",
+ title = "View of Computer Algebra Data from Coq",
+ journal = "Lecture Notes in Computer Science",
+ volume = "6824",
+ pages = "7480",
+ year = "2011",
+ publisher = "SpringerVerlag",
+ abstract =
+ "Data representation is an important aspect of software com
+ position. It is often the case that different software components are
+ pro grammed to represent data in the ways which are the most
+ appropriate for their problem domains. Sometimes, converting data from
+ one repre sentation to another is a nontrivial task. This is the
+ case with computer algebra systems and typetheory based interactive
+ theorem provers such as Coq. We provide some custom instrumentation
+ inside Coq to support a computer algebra system (CAS) communication
+ protocol known as SC SCP. We describe general aspects of viewing
+ OpenMath terms produced by a CAS in the calculus of Coq, as well as
+ viewing pure Coq terms in a simpler type system that is behind OpenMath.",
+ paper = "Kome11.pdf"
+}
+
+\end{chunk}
+
\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@phdthesis{Kreb15,
@@ 15070,6 +15250,19 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\subsection{H} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\index{Hong, Hoon}
+\begin{chunk}{axiom.bib}
+@misc{Hong05,
+ author = "Hong, Hoon",
+ title = "Tutorial on CAD",
+ year = "2005",
+ paper = "Hong05.pdf"
+}
+
+\end{chunk}
+
\subsection{L} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{LaValle, Steven M.}
@@ 22068,7 +22261,8 @@ VM/370 SPAD.SCRIPTS August 24, 1979 SPAD.SCRIPT
number = "4",
pages = "259270",
year = "2002",
 link = "\url{http://www.calculemus.net/meetings/siena01/Papers/Davenport.pdf}",
+ link =
+ "\url{http://www.calculemus.net/meetings/siena01/Papers/Davenport.pdf}",
abstract =
"Equality is such a fundamental concept in mathematics that, in
fact, we seldom explore it in detail, and tend to regard it as
diff git a/changelog b/changelog
index 80065fa..f8824b4 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,7 @@
+20170527 tpd src/axiomwebsite/patches.html 20170527.01.tpd.patch
+20170527 tpd bookvolbib reference for Cylindrical Algebraic Decomposition
+20170526 tpd src/axiomwebsite/patches.html 20170526.01.tpd.patch
+20170526 tpd bookvolbib reference for proofs
20170523 tpd src/axiomwebsite/patches.html 20170523.01.tpd.patch
20170523 tpd bookvolbib reference to Axiom in publications
20170521 tpd src/axiomwebsite/patches.html 20170521.01.tpd.patch
diff git a/patch b/patch
index 77c0a9c..102ed30 100644
 a/patch
+++ b/patch
@@ 1,267 +1,14 @@
bookvolbib reference to Axiom in publications
+bookvolbib reference for Cylindrical Algebraic Decomposition
Goal: Proving Axiom Correct
+Goal: Axiom Algebra
\index{Wright, Francis J.}
+\index{Hong, Hoon}
\begin{chunk}{axiom.bib}
@misc{Wrig03,
 author = "Wright, Francis J.",
 title = "Mathematics and Algorithms for Computer Algebra: Part 1",
 link = "\url{https://people.eecs.berkeley.edu/~fateman/282/F%20Wright%20notes/week1.pdf}",
 year = "2003",
 comment = "full course. week2=Wrig03a, wee3=Wrig03b,...week8=Wrig3g.pdf",
 abstract =
 "This course will be mainly mathematics, some computer science
 and a little computing. Little or no essential use will be made of
 actual computer languages, although I may occasionally use Pascal, C,
 Lisp or REDUCE for concrete examples. The aim of the course is to
 provide an entry into the current research literature, but not to present
 the most recent research results.

 The first half of the course (taught by me) will deal with basic math
 ematics and algorithms for computer algebra, primarily at the level of
 arithmetic and elementary abstract algebra, including an introduction
 to GCDs and the solution of univariate polynomial equations. This
 leads into the second half of the course (taught by Dr Jim Skea) on
 the more advanced problems of polynomial factorization, indefinite in
 tegration, multivariate polynomial equations, etc.

 The first week provides an introduction to the computing aspects
 of computer algebra, and contains almost no mathematics. It is in
 tended to show how the later theory can be implemented for practical
 computation. The second week provides a rapid but superficial survey
 of the abstract algebra that is most important for computer algebra.
 The next five weeks will build on this abstract basis to do some more
 concrete mathematics in more details, referring back to the basis es
 tablished in the first two weeks as necessary.

 At the end of each set of notes will be exercises, one (or more) of
 which will be assessed.",
 paper = "Wrig03.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Brown, W. S.}
\begin{chunk}{axiom.bib}
@articla{Brow78,
 author = "Brown, W. S.",
 title = "The Subresultant PRS Algorithm",
 journal = "ACM Transactions on Mathematical Software",
 volume = "4",
 number = "3",
 year = "1978",
 pages = "237249",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/brown.pdf}",
 abstract =
 "Two earlier papers described the generalizations of Euclid's
 algorithm to deal with the problem of computing the greatest common
 divisor (GCD) or the resultant of a pair of polynomials. A sequal to
 those two papers is presented here.

 In attempting such a generalization one easily arrives at the concept
 of a polynomial remainder sequence (PRS) and then quickly discovers
 the phenomenon of explosive coefficient growth. Fortunately, this
 explosive growth is not inherent in the problem, but is only an
 artifact of various naive solutions. If one removes the content (that
 is, the GCD of the coefficients) from each polynomial in a PRS, the
 coefficient growth in the resulting primitive PRS is relatively modest.
 However, the cost of computing the content (by applying Euclid's
 algorithm in the coefficient domain) may be unacceptably or even
 prohibitively high, especially if the coefficients are themselves
 polynomials in one or more addltional variables.

 The key to controlling coefficient growth without the costly
 computation of GCD's of coefficients is the fundamental theorem of
 subresuitants, which shows that every polynomial in a PRS is
 proportional to some subresultant of the first two. By arranging for
 the constants of proportionahty to be unity, one obtains the
 subresultant PRS algorithm, in which the coefficient growth is
 essentially linear. A corollary of the fundamental theorem is given
 here, which leads to a simple derivation and deeper understanding of
 the subresultant PRS algorithm and converts a conjecture mentioned in
 the earlier papers into an elementary remark.

 A possible alternative method of constructing a subresultant PRS is to
 evaluate all the subresultants directly from Sylvester's determinant
 via expansion by minors. A complexity analysis is given in conclusion,
 along lines pioneered by Gentleman and Johnson, showing that the
 subresultant PRS algorithm is superior to the determinant method
 whenever the given polynomials are sufficiently large and dense, but
 is inferior in the sparse extreme.",
 paper = "Brow78.pdf"
}

\end{chunk}

\index{Collins, George E.}
\begin{chunk}{axiom.bib}
@article{Coll87,
 author = "Collins, George E.",
 title = "Subresultants and Reduced Polynomial Remainder Sequences",
 journal = "J. ACM",
 volume = "14",
 number = "1",
 year = "1987",
 pages = "128142",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/collins.pdf}",
 paper = "Coll87.pdf"
}

\end{chunk}

\index{Gentleman, W. M.}
\index{Johnson, S. C.}
@article{Gent76,
 author = "Gentleman, W. M. and Johnson, S. C.",
 title = "Analysis of Algorithms, A Case Study: Determinants of Matrices
 With Polynomial Entries",
 journal = "ACM Transactions on Mathematical Software",
 volume = "2",
 number = "3",
 year = "1976",
 pages = "232241",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/gentleman.pdf}",
 abstract =
 "The problem of computing the deternunant of a matrix of polynomials
 is considered; two algorithms (expansion by minors and expansion by
 Gaussian elimination) are compared; and each is examined under two models
 for polynomial computatmn (dense univariate and totally sparse). The
 results, while interesting in themselves, also serve to display two
 points: (1) Asymptotic results are sometimes misleading for noninfinite
 (e.g. practical) problems. (2) Models of computation are by
 definition simplifications of reality: algorithmic analysis should be
 carried out under several distinct computatmnal models and should be
 supported by empirical data.",
 paper = "Gent76.pdf"
}

\end{chunk}

\index{Fateman, Richard}
\begin{chunk}{axiom.bib}
@misc{Fate00b,
 author = "Fateman, Richard",
 title = "The (finite field) Fast Fourier Transform",
 year = "2000",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/fftnotes.pdf}",
 abstract =
 "There are numerous directions from which one can approach the subject
 of the fast Fourier Transform (FFT). It can be explained via numerous
 connections to convolution, signal processing, and various other
 properties and applications of the algorithm. We (along with
 Geddes/Czapor/Labahn) take a rather simple view from the algebraic
 manipulation standpoint. As will be apparent shortly, we relate the
 FFT to the evaluation of a polynomial. We also consider it of interest
 primarily as an algorithm in a discrete (finite) computation structure
 rather than over the complex numbers.",
 paper = "Fate00b.pdf"
}

\end{chunk}

\index{Fateman, Richard}
\begin{chunk}{axiom.bib}
@misc{Fate00c,
 author = "Fateman, Richard",
 title = "Additional Notes on Polynomial GCDs, Hensel construction",
 year = "2000",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/hensel.pdf}",
 paper = "Fate00c.pdf"
}

\end{chunk}

\index{Liska, Richard}
\index{Drska, Ladislav}
\index{Limpouch, Jiri}
\index{Sinor, Milan}
\index{Wester, Michael J.}
\index{Winkler, Franz}
\begin{chunk}{axiom.bib}
@book{Lisk99,
 author = "Liska, Richard and Drska, Ladislav and Limpouch, Jiri and
 Sinor, Milan adn Wester, Michael and Winkler, Franz",
 title = "Computer Algebra  Algorithms, Systems and Applications",
 year = "1999",
 publisher = "web",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/liska.pdf}",
 paper = "Lisk99.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Mishra, Bhubaneswar}
\index{Yap, Chee}
\begin{chunk}{axiom.bib}
@misc{Mish87,
 author = "Mishra, Bhubaneswar and Yap, Chee",
 title = "Notes on Groebner Basis",
 year = "1987",
 link = "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/mishra87note.pdf}",
 abstract =
 "We present a selfcontained exposition of the theory of Groebner
 basis and its applications",
 paper = "Mish87.pdf"
}

\end{chunk}

\index{Monagan, Michael}
\index{Wittkopf, Allan D.}
@inproceedings{Mona00,
 author = "Monagan, Michael and Wittkopf, Allan D.",
 title = "On the Design and Implementation of Brown's Algorithm over the
 Integers and Number Fields",
 booktitle = "ISSAC 2000",
 pages = "225233",
 year = "2000",
 isbn = "1581132182",
 abstract =
 "We study the design and implementation of the dense modular GCD
 algorithm of Brown applied to bivariate polynomial GCDs over the
 integers and number fields. We present an improved design of Brown's
 algorithm and compare it asymptotically with Brown's original
 algorithm, with GCDHEU, the heuristic GCD algorithm, and with the
 EEZGCD algorithm. We also make an empirical comparison based on Maple
 implementations of the algorithms. Our findings show that a careful
 implementation of our improved version of Brown's algorithm is much
 better than the other algorithms in theory and in practice.",
 paper = "Mona00.pdf"
}

\end{chunk}

\index{Yap, CheeKeng}
\begin{chunk}{axiom.bib}
@misc{Yap02a,
 author = "Yap, CheeKeng",
 title = "Lecture 0: Introduction",
 year = "2002",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/yap0.pdf}",
 paper = "Yap02a.pdf"
}

\end{chunk}

\index{Yap, CheeKeng}
\begin{chunk}{axiom.bib}
@misc{Yap02b,
 author = "Yap, CheeKeng",
 title = "Lecture II: The GCD",
 year = "2002",
 link =
 "\url{https://people.eecs.berkeley.edu/~fateman/282/readings/yap2.pdf}",
 paper = "Yap02b.pdf"
+@misc{Hong05,
+ author = "Hong, Hoon",
+ title = "Tutorial on CAD",
+ year = "2005",
+ paper = "Hong05.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index a6030f7..c7b9326 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5740,6 +5740,10 @@ bookvolbib type inferencing for Common Lisp
bookvolbib type inferencing papers
20170523.01.tpd.patch
bookvolbib reference to Axiom in publications
+20170526.01.tpd.patch
+bookvolbib reference for proofs
+20170527.01.tpd.patch
+bookvolbib reference for Cylindrical Algebraic Decomposition

1.7.5.4