From 1cfe6aacf29bfde7042024992314618057eb0da9 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 12 May 2017 15:39:55 0400
Subject: [PATCH] bookvolbib: References to DoCon
Goal: Proving Axiom Correct
\index{Meshveliani, Sergei D.}
\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",
keywords = "axiomref"
}
\end{chunk}
\index{Meshveliani, Sergei D.}
\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"
}
\end{chunk}

books/bookvolbib.pamphlet  144 +++++++++++++++++++++++
changelog  2 +
patch  250 +++++++++++++++++++
src/axiomwebsite/patches.html  6 +
4 files changed, 267 insertions(+), 135 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index b9ab4c2..0870425 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 7810,6 +7810,150 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Meshveliani, Sergei D.}
+\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",
+ keywords = "axiomref"
+}
+
+\end{chunk}
+
+\index{Meshveliani, Sergei D.}
+\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"
+
+}
+
+\end{chunk}
+
\index{Milner, Robin}
\begin{chunk}{axiom.bib}
@techreport{Miln72,
diff git a/changelog b/changelog
index 6d7e29c..bd0510a 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+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
20170509 tpd bookvolbib Cylindrical Algebraic Decomposition references
20170507 tpd src/axiomwebsite/patches.html 20170507.01.tpd.patch
diff git a/patch b/patch
index 0834543..0a5864f 100644
 a/patch
+++ b/patch
@@ 1,164 +1,148 @@
bookvolbib: Cylindrical Algebraic Decomposition references
+bookvolbib: References to DoCon
Goal: Proving Axiom Correct
\index{Brown, Christopher W.}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Brow12,
 author = "Brown, Christopher W.",
 title = "Fast simplifications for Tarski formulas based on monomial
 inequalities",
 year = "2012",
 journal = "Journal of Symbolic Computation",
 volume = "47",
 pages = "859882",
 abstract =
 "We define the ‘‘combinatorial part’’ of a Tarski formula in which
 equalities and inequalities are in factored or partially factored
 form. The combinatorial part of a formula contains only
 ‘‘monomial inequalities’’,which are sign conditions on monomials. We
 give efficient algorithms for answering some basic questions about
 conjunctions of monomial inequalities and prove the
 NPCompleteness/Hardness of some others. By simplifying the
 combinatorial part of a Tarski formula, and mapping the simplified
 combinatorial part back to a Tarski formula, we obtain nontrivial
 simplifications without algebraic operations.",
 paper = "Brow12.pdf"
+@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{Arno, D.S.}
\index{Mignotte, M.}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Arno88,
 author = "Arno, D.S. and Mignotte, M.",
 title = "On Mechanical Quantifier Elimination for Elementary Algebra
 and Geometry",
 journal = "J. Symbolic Computation",
 volume = "5",
 pages = "237259",
 year = "1988",
 link = "\url{http://http://www.sciencedirect.com/science/article/pii/S0747717188800142/pdf?md5=62052077d84e6078cc024bc8e29c23c1&pid=1s2.0S0747717188800142main.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
 polynomial function $f(x)=x^4+px^2+qx+r$ is nonnegative for all real
 $x$ and (2) find conditions on real numbers $a$, $b$, and $c$ so that
 the ellipse $\frac{(xe)^2}{q^2}+\frac{y^2}{b^2}1=0$ lies inside the
 unit circle $y^2+x^21=0$. Our solutions are obtained by following the
 basic outline of the method of quantifier elimination by cylindrical
 algebraic decomposition (Collins, 1975), but we have developed, and
 have been considerably aided by, modified versions of certain of its
 steps. We have found three equally simple but not obviously equivalent
 solutions for the first problem, illustrating the difficulty of
 obtaining unique ``simplest'' solutions to quantifier elimination
 problems of elementary algebra and geometry.",
 paper = "Arno88.pdf"

+@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{Collins, George E.}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Coll75,
 author = "Collins, George E.",
 title = "Quantifier Elimination for Real Closed Fields by
 Cylindrical Algebraic Decomposition",
 year = "1975",
 journal = "Lecture Notes in Computer Science",
 volume = "33",
 pages = "134183",
+@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 =
 "I. Introduction. Tarski in 1948, published a quantifier
 elimination method for the elementary theory of real closed fields
 (which he had discoverd in 1930). As noted by Tarski, any quantifier
 elimination method for this theory also provides a decision method,
 which enables one to decide whether any sentence of the theory is
 true or false. Since many important and difficult mathematical
 problems can be expressed in this theory, any computationally
 feasible quantifier elimination algorithm would be of utmost
 significance.

 However, it became apparent that Tarski's method required too much
 computation to be practical except for quite trivial problems.
 Seidenberg in 1954, described another method which he thought
 would be more efficient. A third method was published by Cohen in
 1969. Some significant improvements of Tarski's method have been
 made by W. Boge, which are described in a thesis by Holthusen

 This paper describes a completely new method which I discoverd in
 February 1973. This method was presented in a seminar at Stanford
 University in March 1973 and in abstract form at a symposium at
 CarnegieMellon University in May 1973. In August 1974 a full
 presentation of the method was delivered at the EUROSAM 74 Conference
 in Stockholm, and a preliminary version of the present paper was
 published in the proceedings of that conference.",
 paper = "Coll75.pdf"
+ "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",
+ keywords = "axiomref"
}
\end{chunk}
\index{Arnon, Dennis S.}
\index{Collins, George E.}
\index{McCallum, Scott}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@techreport{Arno82,
 author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
 title = "Cylindrical Algebraic Decomposition I: The Basic Algorithm",
 year = "1982",
 institution = "Purdue University",
 type = "Technical Report",
 number = "82427A",
 link = "\url{https://pdfs.semanticscholar.org/7643/4b54250f05ebf0dcc27c33b7dc250419fb94.pdf}",
 abstract =
 "Given a set of rvariate integral polynomials, a {\sl cylindrical
 algebraic decomposition (cad)} of euclidean rspace $E^r$ into connected
 subsets compatible with the zeros of the polynomials. Collins gave a
 cad construction algorithm in 1975, as part of a quantifier elimination
 procedure for real closed fields. The algorithm has subsequently found
 diverse applications (optimization, curve display); new applications
 have been proposed (term rewriting systems, motion planning). In the
 present twopart paper, we give an algorithm for determining the pairs
 of adjacent cells in a cad of $E^2$. This capability is often needed
 in applications. In Part I we describe the essential features of the
 rspace cad algorithm, to provide a framework for the adjacency algorithm
 in Part II.",
 paper = "Arno82.pdf"
+@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{Arnon, Dennis S.}
\index{Collins, George E.}
\index{McCallum, Scott}
+\index{Meshveliani, Sergei D.}
\begin{chunk}{axiom.bib}
@article{Arno84,
 author = "Arnon, Dennis S. and Collins, George E. and McCallum, Scott",
 title = "Cylindrical Algebraic Decomposition II: An Adjacency Algorithm
 for the Plane",
 year = "1984",
 journal = "SIAM J. Comput.",
 volume = "13",
 number = "4",
 pages = "878889",
 abstract =
 "Given a set of rvariate integral polynomials, a {\sl cylindrical
 algebraic decomposition (cad)} of euclidean rspace $E^r$ partitions
 $E^r$ into connected subsets compaitible with the zeros of the
 polynomials. Each subset is a {\sl cell}. Informally, two cells of
 a cad are {\sl adjacent} if they touch each other; formally, they are
 adjacent if their union is connected. In applications of cad's one
 often wishes to know the adjacent pairs of cells. Previous algorithms
 for cad construction (such as that given in Part I of this paper) have
 not actually determined them. We give here in Part II an algorithm
 which determines the pairs of adjacent cells as it constructs a cad
 of $E^2$.",
 paper = "Arno84.pdf"
+@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"
+
+}
+\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index cabdafd..7e0b09f 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5711,9 +5711,11 @@ src/axiomwebsite/download.html fix typo in BSD binary filename
20170417.04.bmt.patch
Makefile Build patches for BSD distribution on MAC OSX
20170507.01.tpd.patch
bookvolbib Add references to Axiom in literature
+bookvolbib Add references to Axiom in literature
20170509.01.tpd.patch
bookvolbib Cylindrical Algebraic Decomposition references
+bookvolbib Cylindrical Algebraic Decomposition references
+20170512.01.tpd.patch
+bookvolbib References to DoCon

1.7.5.4