From d1e7a0fe1ff036ecc48f0a40c48cedfe16916038 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 12 May 2017 18:09:42 0400
Subject: [PATCH] bookvolbib Cylindrical Algebraic Decomposition references
Goal: Axiom Algebra
\index{Caviness, B. F.}
\index{Johnson, J. R.}
\begin{chunk}{axiom.bib}
@book{Cavi98,
author = "Caviness, B. F. and Johnson, J. R.",
title = "Quantifier Elimination and Cylindrical Algebraic Decomposition",
publisher = "Springer",
year = "1998",
isbn = "3221827943",
keywords = "axiomref"
}
\end{chunk}
\index{Brown, Christopher W.}
\begin{chunk}{axiom.bib}
@article{Brow01a,
author = "Brown, Christopher W.",
title = "Simple CAD Construction and its Applications",
journal = "J. Symbolic Computation",
year = "2001",
volume = "31",
pages = "521547",
abstract =
"This paper presents a method for the simplification of truthinvariant
cylindrical algebraic decompositions (CADs). Examples are given that
demonstrate the usefulness of the method in speeding up the solutoin
formula construction phase of the CADbased quantifier elimination
algorithm. Applications of the method to the construction of
truthinvariant CADs for very large quantifierfree formulas and
quantifier elimination of nonprenex formulas are also discussed.",
paper = "Brow01a.pdf"
}
\end{chunk}

books/bookvolbib.pamphlet  36 +++++++++
changelog  2 +
patch  162 +++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 67 insertions(+), 135 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 0870425..3de642b 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 14385,6 +14385,28 @@ Proc ISSAC 97 pp172175 (1997)
\index{Brown, Christopher W.}
\begin{chunk}{axiom.bib}
+@article{Brow01a,
+ author = "Brown, Christopher W.",
+ title = "Simple CAD Construction and its Applications",
+ journal = "J. Symbolic Computation",
+ year = "2001",
+ volume = "31",
+ pages = "521547",
+ abstract =
+ "This paper presents a method for the simplification of truthinvariant
+ cylindrical algebraic decompositions (CADs). Examples are given that
+ demonstrate the usefulness of the method in speeding up the solutoin
+ formula construction phase of the CADbased quantifier elimination
+ algorithm. Applications of the method to the construction of
+ truthinvariant CADs for very large quantifierfree formulas and
+ quantifier elimination of nonprenex formulas are also discussed.",
+ paper = "Brow01a.pdf"
+}
+
+\end{chunk}
+
+\index{Brown, Christopher W.}
+\begin{chunk}{axiom.bib}
@misc{Brow02,
author = "Brown, Christopher W.",
title = "QEPCAD B  A program for computing with semialgebraic sets
@@ 14407,6 +14429,20 @@ Proc ISSAC 97 pp172175 (1997)
\end{chunk}
+\index{Caviness, B. F.}
+\index{Johnson, J. R.}
+\begin{chunk}{axiom.bib}
+@book{Cavi98,
+ author = "Caviness, B. F. and Johnson, J. R.",
+ title = "Quantifier Elimination and Cylindrical Algebraic Decomposition",
+ publisher = "Springer",
+ year = "1998",
+ isbn = "3221827943",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
\index{Chen, Changbo}
\index{Davenport, James H.}
\index{May, John P.}
diff git a/changelog b/changelog
index bd0510a..f1adccb 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170512 tpd src/axiomwebsite/patches.html 20170512.02.tpd.patch
+20150512 tpd bookvolbib Cylindrical Algebraic Decomposition references
20170512 tpd src/axiomwebsite/patches.html 20170512.01.tpd.patch
20170512 tpd bookvolbib References to DoCon
20170509 tpd src/axiomwebsite/patches.html 20170509.01.tpd.patch
diff git a/patch b/patch
index 0a5864f..cf1972e 100644
 a/patch
+++ b/patch
@@ 1,147 +1,39 @@
bookvolbib: References to DoCon
+bookvolbib Cylindrical Algebraic Decomposition references
Goal: Proving Axiom Correct
+Goal: Axiom Algebra
\index{Meshveliani, Sergei D.}
+\index{Caviness, B. F.}
+\index{Johnson, J. R.}
\begin{chunk}{axiom.bib}
@inproceedings{Mesh01,
 author = "Meshveliani, Sergei D.",
 title = "Computer Algebra with Haskell: Applying
 FunctionalCategorical`Lazy' Programming",
 booktitle = "Computer Algebra and its Application to Physics",
 year = "2001",
 pages = "203211",
 link =
 "\url{compalg.jinr.ru/Confs/CAAP\_2001/Final/proceedings/proceed.pdf}",
 abstract =
 "We give an outline of a computer algebra program writting in a
 functional language Haskell and implementing certain piece of
 commutative algebra",
 paper = "Mesh01.pdf",
 keywords = "axiomref"

}

\end{chunk}

\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@misc{Mesh10,
 author = "Meshveliani, Sergei D.",
 title = "Haskell and computer algebra",
 link = "\url{http://www.botik.ru/pub/local/Mechveliani/basAlgPropos/haskellinCA2.pdf.zip}",
 year = "2010",
 abstract =
 "We consider the ways to program mathematics in the Haskell language.
 To start a discussion, we pretend to propose certain basic algebra
 library BAL for Haskell. We also mention several desirable language
 features. Algebraic additions in BAL are divided into the 'ordinary'
 and 'advanced'. Standard algebraic classes are reorganized to make
 them mathematically meaningful. For the 'advanced' part a sample
 argument approach is introduced  as certain alternative for the
 dependent type language extension. The library is implemented in the
 existing Haskell, by 'hiding' a certain part of the existing Prelude.",
 paper = "Mesh10.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Mesh14,
 author = "Meshveliani, Sergei D.",
 title = "On dependent types and intuitionism in programming mathematics",
 journal = "Program systems: theory and applications",
 year = "2014",
 volume = "5",
 numbrer = "3(21)",
 pages = "2750",
 comment = "(In Russian)",
 link = "\url{http://psta.psiras.ru/read/psta2014_3_2750.pdf}",
 abstract =
 "It is discussed a practical possibility of a provable programming
 of mathematics basing of the approach of intuitionism, a language
 with dependent types, proofcarrying code. This approach is
 illustrated with examples. The discourse bases on the experience
 of implementing in the {\tt Agda} language of a certain small
 algebraic library including the arithmetic of a residue domain
 $R/(b)$ for an arbitrary Euclidean ring R. (In Russian)",
 paper = "Mesh14.pdf",
+@book{Cavi98,
+ author = "Caviness, B. F. and Johnson, J. R.",
+ title = "Quantifier Elimination and Cylindrical Algebraic Decomposition",
+ publisher = "Springer",
+ year = "1998",
+ isbn = "3221827943",
keywords = "axiomref"
}
\end{chunk}
\index{Meshveliani, Sergei D.}
+\index{Brown, Christopher W.}
\begin{chunk}{axiom.bib}
@article{Mesh15,
 author = "Meshveliani, Sergei D.",
 title = "Programming basic computer algebra in a language with
 dependent types",
 journal = "Program systems: theory and applications",
 year = "2015",
 volume = "6",
 numbrer = "4(27)",
 pages = "313340",
 comment = "(In Russian)",
 link = "\url{http://psta.psiras.ru/read/psta2015_4_313340.pdf}",
 abstract =
 "It is described the experience in provable programming of certain
 classical categories of computational algebra (``group'', ``ring'',
 and so on) basing on the approach of intuitionism, a language with
 dependent types, forming of machinechecked proofs. There are detected
 the related problems, and are described certain additional possibilities
 given by the approach. The {\tt Agda} functional language is used as an
 instrument. This paper is a continuation for the introductory paper
 published in this journal in 2014. (In Russian)",
 paper = "Mesh15.pdf"
}

\end{chunk}

\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@book{Mesh16,
 author = "Meshveliani, Sergei D.",
 title = "DoConA a Provable Algebraic Domain Constructor",
 link =
 "\url{http://www.botik.ru/pub/local/Mechveliani/doconA/0.04/manual.pdf}",
 publisher = "User Manual, Version 0.04",
 year = "2016",
 abstract =
 "This book is about 1) a manual on the DoConA program library, 2) a book
 explaining how to program algebra in a purely functional language with
 {\sl dependent types} (specifially, in {\tt Agda}), with providing
 machinechecked proofs, and following constructive mathematics.

 The above point of proofs means that a program not only implements an
 algorithm, but explains to the compiler the needed mathematical notions
 and provides the needed proofs in the form of type expressions and
 functions. And the compiler (more precisely, type checker) is able to
 verify these proofs statically (before running), and to prepare the
 algorithm for running.",
 paper = "Mesh16,pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@misc{Mesh16a,
 author = "Meshveliani, Sergei D.",
 title = "Provable programming of algebra: particular points, examples",
 link = "\url{http://www.botik.ru/pub/local/Mechveliani/provProgExam.zip}",
 year = "2016",
 abstract =
 "It is discussed an experiance in provable programming of a computer
 algebra library with using a purely functional language with dependent
 tyhpes ({\tt Agda}). There are given several examples illustrating
 particular points of implementing the approach of constructive
 mathematics.",
 paper = "Mesh16a.pdf"

+@article{Brow01a,
+ author = "Brown, Christopher W.",
+ title = "Simple CAD Construction and its Applications",
+ journal = "J. Symbolic Computation",
+ year = "2001",
+ volume = "31",
+ pages = "521547",
+ abstract =
+ "This paper presents a method for the simplification of truthinvariant
+ cylindrical algebraic decompositions (CADs). Examples are given that
+ demonstrate the usefulness of the method in speeding up the solutoin
+ formula construction phase of the CADbased quantifier elimination
+ algorithm. Applications of the method to the construction of
+ truthinvariant CADs for very large quantifierfree formulas and
+ quantifier elimination of nonprenex formulas are also discussed.",
+ paper = "Brow01a.pdf"
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 7e0b09f..f7e1670 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5716,6 +5716,8 @@ bookvolbib Add references to Axiom in literature
bookvolbib Cylindrical Algebraic Decomposition references
20170512.01.tpd.patch
bookvolbib References to DoCon
+20170512.02.tpd.patch
+bookvolbib Cylindrical Algebraic Decomposition references

1.7.5.4