From 48122d4dc97ee8de28a20e07f01d2a5cc98d180c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 27 Jun 2016 17:26:28 0400
Subject: [PATCH] books/bookvolbib Axiom Citations in the Literature
Goal: Axiom Literate Programming
\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@InProceedings{Koep99,
author = "Koepf, Wolfram",
title = "Orthogonal polnomials and computer algebra",
booktitle = "Recent developments in complex analysis and computer algebra",
series = "ISSAC 97",
year = "1999",
publisher = "Kluwer Adademic Publishers",
location = "Newark, DE",
pages = "205234",
keywords = "axiomref",
paper = "Koep99.pdf",
abstract =
"Orthogonal polynomials have a long history, and are still important
objects of consideration in mathematical research as well as in
applications in Mathematical Physics, Chemistry, and
Engineering. Quite a lot is known about them. Particularly wellknown
are differential equations, recurrence equations, Rodrigues formulas,
generating functions and hypergeometric representations for the
classical systems of Jacobi, Laguerre and Hermite which can be found
in mathematical dictionaries. Less wellknown are the corresponding
representations for the classical discrete systems of Hahn,
Krawtchouk, Meixner and Charlier, as well as addition theorems,
connection relations between different systems and other identities
for these and other systems of orthogonal polynomials. The ongoing
research in this still very active subject of mathematics expands the
knowledge database about orthogonal polynomials continuously. In the
last few decades the classical families have been extended to a rather
large collection of polynomial systems, the socalled AskeyWilson
scheme, and they have been generalized in other ways as well.
Recently new algorithmic approaches have been discovered to compute
differential, recurrence and similar equations from series or integral
representations. These methods turn out to be quite useful to prove or
detect identities for orthogonal polynomial systems. Further
algorithms to detect connection coefficients or to identify polynomial
systems from given recurrence equations have been developed. Although
some algorithmic methods had been known already in the last century,
their use was rather limited due to the immense amount of
calculations. Only the existence and distribution of computer algebra
systems makes their use simple and useful for everybody.
In this plenary lecture an overview is given of how algorithmic
methods implemented in computer algebra systems can be used to prove
identities about and to detect new knowledge for orthogonal
polynomials and other hypergeometric type special functions.
Implementations for this type of algorithms exist in Maple,
Mathematica and REDUCE, and maybe also in other computer algebra
systems. Online demonstrations will be given using Maple V.5."
}
\end{chunk}
\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@misc{Koep14,
author = "Koepf, Wolfram",
title = "Methods of Computer Algebra for Orthogonal Polynomials",
year = "2014",
location = "Rutgers, NJ, USA",
url =
"http://www.mathematik.unikassel.de/~koepf/Vortrag/2014ZeilbergerVortrag.pdf",
paper = "Koep14.pdf",
video1 = "https://vimeo.com/85573338",
video2 = "https://vimeo.com/85573712",
website = "http://www.caop.org"
}
\end{chunk}
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
@misc{Daly08,
author = "Daly, Timothy",
title = "Axiom Computer Algebra System Information Sources",
video = "https://www.youtube.com/watch?v=CV8y3UrpadY",
keywords = "axiomref",
year = "2008"
}
\end{chunk}
\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@article{Koep99a,
author = "Koepf, Wolfram",
title = "Software for the algorithmic work with orthogonal polynomials
and special functions",
journal = "Electron. Trans. Numer. Anal.",
volume = "9",
year = "1999",
keywords = "axiomref",
paper = "Koep99a.pdf",
url = "http://arxiv.org/pdf/math/9809125v1.pdf",
abstract =
"An overview of the MAPLE routines that can be used for hypergeometric
and basic hypergeometric series with some discussion of how and why
they work."
}
\end{chunk}
\index{Martin, Ursula}
\begin{chunk}{axiom.bib}
@InProceedings{Mart99,
author = "Martin, Ursula",
title = "Computers, reasoning and mathematical practice",
booktitle = "Computational Logic",
publisher = "Springer",
year = "1999",
location = "Marktoberdorf, Germany",
pages = "301346",
keywords = "axiomref",
paper = "Mart99.pdf",
url =
"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.2061&rep=rep1&type=pdf",
abstract =
"We identify three main objectives for computer aided reasoning
enhancing the techniques available for mathematical experimentation,
developing community standards for experiment and modelling and
developing methods which will make computation more acceptable as part
of a proof. We discuss three areas of research which address these:
the use of theorem proving techniques to enhance or extend
mathematical software systems, support for formal methods techniques
to increase the reliability of such systems, and the use of computer
aided formal reasoning in support of mathematical practice. This last
includes activities such as formalizing systems for computational
mathematics or visualization so that they can still be used informally
but generate a formal development, and developing techniques to
provide assistance in the initial stages of developing a new theory.
By mathematics here we mean the activities of working research
mathematicians, producing new results in pure or applied mathematics,
although we touch briefly on some questions concerning the
applications of computational mathematics and simulation in research
science and engineering. We have left out several other related areas
entirely: logical questions of decidability, soundness or
completeness, theoretical computer science issues of semantics,
computability or complexity, foundational issues such as
constructivity, computer aided proofs about software and hardware, and
the use of computers in mathematical education at all levels and in
heuristic discovery. In particular foundational questions about
computation have transformed mathematical logic, computation has made
constructive proof feasible, and effective notions of practice for
proofs about hardware and software are by no means well understood.
However these matters fall outside the scope of this paper."
}
\end{chunk}
\index{Brown, Ronald}
\index{Tonks, Andrew}
\begin{chunk}{axiom.bib}
@article{Brow94,
author = "Brown, Ronald and Tonks, Andrew",
title = "Calculations with simplicial and cubical groups in AXIOM",
journal = "Journal of Symbolic Computation",
volume = "17",
number = "2",
pages = "159179",
year = "1994",
month = "February",
misc = "CODEN JSYCEH ISSN 07477171",
keywords = "axiomref",
paper = "Brow94.pdf",
abstract =
"Work on calculations with simplical and cubical groups in AXIOM was
carried out using loan equipment and software from IBM UK and guidance
from L. A. Lambe. We report on the results of this work, and present
the AXIOM code written by the second author during this period. This
includes an implementation of the monoids which model cubes and
simplices, together with a new AXIOM category of nearrings with which
to carry out nonabelian calculations. Examples of the use of this
code in interactive AXIOM sessions are also given."
}
\end{chunk}

books/bookvolbib.pamphlet  177 +++++++++++++++++++++++
changelog  2 +
patch  295 ++++++++++++++++++++
src/axiomwebsite/patches.html  2 +
4 files changed, 319 insertions(+), 157 deletions()
diff git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index dd9752f..4adfd54 100644
 a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ 4558,11 +4558,11 @@ Martin, U.
\end{chunk}
\index{Boulm\'e, S.}
\index{Hardin, T.}
\index{Hirschkoff, D.}
+\index{Boulm\'e, Sylvain}
+\index{Hardin, Therese}
+\index{Hirschkoff, Daniel}
\index{Rioboo, Renaud}
\index{M\'enissierMorain, V.}
+\index{M\'enissierMorain, Valerie}
\begin{chunk}{axiom.bib}
@InProceedings{Boul99,
author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
@@ 11485,10 +11485,10 @@ Elektronik, 43(15) CODEN EKRKAR ISSN 00135658
\end{chunk}
\index{Brown, Ronald}
\index{Tonks, A.}
+\index{Tonks, Andrew}
\begin{chunk}{axiom.bib}
@article{BT94,
 author = "Brown, R. and Tonks, A.",
+@article{Brow94,
+ author = "Brown, Ronald and Tonks, Andrew",
title = "Calculations with simplicial and cubical groups in AXIOM",
journal = "Journal of Symbolic Computation",
volume = "17",
@@ 11497,7 +11497,17 @@ Elektronik, 43(15) CODEN EKRKAR ISSN 00135658
year = "1994",
month = "February",
misc = "CODEN JSYCEH ISSN 07477171",
 keywords = "axiomref"
+ keywords = "axiomref",
+ paper = "Brow94.pdf",
+ abstract =
+ "Work on calculations with simplical and cubical groups in AXIOM was
+ carried out using loan equipment and software from IBM UK and guidance
+ from L. A. Lambe. We report on the results of this work, and present
+ the AXIOM code written by the second author during this period. This
+ includes an implementation of the monoids which model cubes and
+ simplices, together with a new AXIOM category of nearrings with which
+ to carry out nonabelian calculations. Examples of the use of this
+ code in interactive AXIOM sessions are also given."
}
\end{chunk}
@@ 12082,6 +12092,18 @@ In Wang [Wan92] pp369375 ISBN 0897914899 (soft cover) 0897914902
\index{Daly, Timothy}
\begin{chunk}{axiom.bib}
+@misc{Daly08,
+ author = "Daly, Timothy",
+ title = "Axiom Computer Algebra System Information Sources",
+ video = "https://www.youtube.com/watch?v=CV8y3UrpadY",
+ keywords = "axiomref",
+ year = "2008"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}
@misc{Daly88,
author = "Daly, Timothy",
title = "Axiom in an Educational Setting, Axiom course slide deck",
@@ 14389,6 +14411,97 @@ University of St Andrews, 6th April 2000
\end{chunk}
+\index{Koepf, Wolfram}
+\begin{chunk}{axiom.bib}
+@InProceedings{Koep99,
+ author = "Koepf, Wolfram",
+ title = "Orthogonal polnomials and computer algebra",
+ booktitle = "Recent developments in complex analysis and computer algebra",
+ series = "ISSAC 97",
+ year = "1999",
+ publisher = "Kluwer Adademic Publishers",
+ location = "Newark, DE",
+ pages = "205234",
+ keywords = "axiomref",
+ paper = "Koep99.pdf",
+ abstract =
+ "Orthogonal polynomials have a long history, and are still important
+ objects of consideration in mathematical research as well as in
+ applications in Mathematical Physics, Chemistry, and
+ Engineering. Quite a lot is known about them. Particularly wellknown
+ are differential equations, recurrence equations, Rodrigues formulas,
+ generating functions and hypergeometric representations for the
+ classical systems of Jacobi, Laguerre and Hermite which can be found
+ in mathematical dictionaries. Less wellknown are the corresponding
+ representations for the classical discrete systems of Hahn,
+ Krawtchouk, Meixner and Charlier, as well as addition theorems,
+ connection relations between different systems and other identities
+ for these and other systems of orthogonal polynomials. The ongoing
+ research in this still very active subject of mathematics expands the
+ knowledge database about orthogonal polynomials continuously. In the
+ last few decades the classical families have been extended to a rather
+ large collection of polynomial systems, the socalled AskeyWilson
+ scheme, and they have been generalized in other ways as well.
+
+ Recently new algorithmic approaches have been discovered to compute
+ differential, recurrence and similar equations from series or integral
+ representations. These methods turn out to be quite useful to prove or
+ detect identities for orthogonal polynomial systems. Further
+ algorithms to detect connection coefficients or to identify polynomial
+ systems from given recurrence equations have been developed. Although
+ some algorithmic methods had been known already in the last century,
+ their use was rather limited due to the immense amount of
+ calculations. Only the existence and distribution of computer algebra
+ systems makes their use simple and useful for everybody.
+
+ In this plenary lecture an overview is given of how algorithmic
+ methods implemented in computer algebra systems can be used to prove
+ identities about and to detect new knowledge for orthogonal
+ polynomials and other hypergeometric type special functions.
+ Implementations for this type of algorithms exist in Maple,
+ Mathematica and REDUCE, and maybe also in other computer algebra
+ systems. Online demonstrations will be given using Maple V.5."
+}
+
+\end{chunk}
+
+\index{Koepf, Wolfram}
+\begin{chunk}{axiom.bib}
+@article{Koep99a,
+ author = "Koepf, Wolfram",
+ title = "Software for the algorithmic work with orthogonal polynomials
+ and special functions",
+ journal = "Electron. Trans. Numer. Anal.",
+ volume = "9",
+ year = "1999",
+ keywords = "axiomref",
+ paper = "Koep99a.pdf",
+ url = "http://arxiv.org/pdf/math/9809125v1.pdf",
+ abstract =
+ "An overview of the MAPLE routines that can be used for hypergeometric
+ and basic hypergeometric series with some discussion of how and why
+ they work."
+}
+
+\end{chunk}
+
+\index{Koepf, Wolfram}
+\begin{chunk}{axiom.bib}
+@misc{Koep14,
+ author = "Koepf, Wolfram",
+ title = "Methods of Computer Algebra for Orthogonal Polynomials",
+ year = "2014",
+ location = "Rutgers, NJ, USA",
+ url =
+"http://www.mathematik.unikassel.de/~koepf/Vortrag/2014ZeilbergerVortrag.pdf",
+ paper = "Koep14.pdf",
+ video1 = "https://vimeo.com/85573338",
+ video2 = "https://vimeo.com/85573712",
+ website = "http://www.caop.org"
+}
+
+\end{chunk}
+
\index{Koseleff, P.V.}
\begin{chunk}{ignore}
\bibitem[Kosleff 91]{Kos91} Koseleff, P.V.
@@ 21213,6 +21326,54 @@ Chapter 8. NPL Notes on Applied Science (2nd Edition). 16 HMSO. 1961
\end{chunk}
+\index{Martin, Ursula}
+\begin{chunk}{axiom.bib}
+@InProceedings{Mart99,
+ author = "Martin, Ursula",
+ title = "Computers, reasoning and mathematical practice",
+ booktitle = "Computational Logic",
+ publisher = "Springer",
+ year = "1999",
+ location = "Marktoberdorf, Germany",
+ pages = "301346",
+ keywords = "axiomref",
+ paper = "Mart99.pdf",
+ url =
+"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.2061&rep=rep1&type=pdf",
+ abstract =
+ "We identify three main objectives for computer aided reasoning
+ enhancing the techniques available for mathematical experimentation,
+ developing community standards for experiment and modelling and
+ developing methods which will make computation more acceptable as part
+ of a proof. We discuss three areas of research which address these:
+ the use of theorem proving techniques to enhance or extend
+ mathematical software systems, support for formal methods techniques
+ to increase the reliability of such systems, and the use of computer
+ aided formal reasoning in support of mathematical practice. This last
+ includes activities such as formalizing systems for computational
+ mathematics or visualization so that they can still be used informally
+ but generate a formal development, and developing techniques to
+ provide assistance in the initial stages of developing a new theory.
+
+ By mathematics here we mean the activities of working research
+ mathematicians, producing new results in pure or applied mathematics,
+ although we touch briefly on some questions concerning the
+ applications of computational mathematics and simulation in research
+ science and engineering. We have left out several other related areas
+ entirely: logical questions of decidability, soundness or
+ completeness, theoretical computer science issues of semantics,
+ computability or complexity, foundational issues such as
+ constructivity, computer aided proofs about software and hardware, and
+ the use of computers in mathematical education at all levels and in
+ heuristic discovery. In particular foundational questions about
+ computation have transformed mathematical logic, computation has made
+ constructive proof feasible, and effective notions of practice for
+ proofs about hardware and software are by no means well understood.
+ However these matters fall outside the scope of this paper."
+}
+
+\end{chunk}
+
\subsection{V} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\index{Van Dooren, P.}
diff git a/changelog b/changelog
index d835d31..4856bfc 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20160627 tpd src/axiomwebsite/patches.html 20160626.03.tpd.patch
+20160627 tpd books/bookvolbib Axiom Citations in the Literature
20160627 tpd src/axiomwebsite/patches.html 20160626.02.tpd.patch
20160627 tpd books/bookvol10.4 additional citations
20160627 tpd books/bookvol10.2 additional citations
diff git a/patch b/patch
index 7c3f9f6..f1687d5 100644
 a/patch
+++ b/patch
@@ 2,184 +2,181 @@ books/bookvolbib Axiom Citations in the Literature
Goal: Axiom Literate Programming
\index{Kumar, P.}
\index{Pellegrino, S.}
+\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@article{Kuma00,
 author = "Kumar, P. and Pellegrino, S.",
 title = "Computation of kinematic paths and bifurcation points",
 journal = "Int. J. Solids Struct.",
 volume = "37",
 number = "4647",
 pages = "70037027",
 year = "2000",
+@InProceedings{Koep99,
+ author = "Koepf, Wolfram",
+ title = "Orthogonal polnomials and computer algebra",
+ booktitle = "Recent developments in complex analysis and computer algebra",
+ series = "ISSAC 97",
+ year = "1999",
+ publisher = "Kluwer Adademic Publishers",
+ location = "Newark, DE",
+ pages = "205234",
keywords = "axiomref",
 abstract =
 "This article deals with the kinematic simulation of movable
 structures that go through special configurations of kinematic
 bifurcation, as they move. A series of algorithms are developed for
 structures that can be modelled using pinjointed bars and that admit
 a singleparameter motion. These algorithms are able to detect and
 locate any bifurcation points that exist along the path of the
 structure and, at each bifurcation point, can determine all possible
 motions of the structure. The theory behind the algorithms is
 explained, and the analysis of a simple example is discussed in
 detail. Then, a simplified version of the particular problem that had
 motivated this work, the simulation of the folding and deployment of a
 thin membrane structure forming a solar sail, is analysed. For the
 particular cases that are considered, it is found that the entire
 process is inextensional, but a detailed study of the simulation
 results shows that in more general cases, it is likely that stretching
 or wrinkling will occur."
+ paper = "Koep99.pdf",
+ abstract =
+ "Orthogonal polynomials have a long history, and are still important
+ objects of consideration in mathematical research as well as in
+ applications in Mathematical Physics, Chemistry, and
+ Engineering. Quite a lot is known about them. Particularly wellknown
+ are differential equations, recurrence equations, Rodrigues formulas,
+ generating functions and hypergeometric representations for the
+ classical systems of Jacobi, Laguerre and Hermite which can be found
+ in mathematical dictionaries. Less wellknown are the corresponding
+ representations for the classical discrete systems of Hahn,
+ Krawtchouk, Meixner and Charlier, as well as addition theorems,
+ connection relations between different systems and other identities
+ for these and other systems of orthogonal polynomials. The ongoing
+ research in this still very active subject of mathematics expands the
+ knowledge database about orthogonal polynomials continuously. In the
+ last few decades the classical families have been extended to a rather
+ large collection of polynomial systems, the socalled AskeyWilson
+ scheme, and they have been generalized in other ways as well.
+
+ Recently new algorithmic approaches have been discovered to compute
+ differential, recurrence and similar equations from series or integral
+ representations. These methods turn out to be quite useful to prove or
+ detect identities for orthogonal polynomial systems. Further
+ algorithms to detect connection coefficients or to identify polynomial
+ systems from given recurrence equations have been developed. Although
+ some algorithmic methods had been known already in the last century,
+ their use was rather limited due to the immense amount of
+ calculations. Only the existence and distribution of computer algebra
+ systems makes their use simple and useful for everybody.
+
+ In this plenary lecture an overview is given of how algorithmic
+ methods implemented in computer algebra systems can be used to prove
+ identities about and to detect new knowledge for orthogonal
+ polynomials and other hypergeometric type special functions.
+ Implementations for this type of algorithms exist in Maple,
+ Mathematica and REDUCE, and maybe also in other computer algebra
+ systems. Online demonstrations will be given using Maple V.5."
}
\end{chunk}
\index{Safouhi, Hassan}
+\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@article{Safo00,
 author = "Safouhi, Hassan",
 title = {The $HD$ and $H\overline{D}$ methods for accelerating the
 convergence of threecenter nuclear attraction and fourcenter
 twoelectron Coulomb integrals over $B$ functions and their
 convergence properties.},
 journal = "J. Comput. Phys.",
 volume = "165",
 number = "2",
 pages = "473495",
 year = "2000",
+@misc{Koep14,
+ author = "Koepf, Wolfram",
+ title = "Methods of Computer Algebra for Orthogonal Polynomials",
+ year = "2014",
+ location = "Rutgers, NJ, USA",
+ url =
+"http://www.mathematik.unikassel.de/~koepf/Vortrag/2014ZeilbergerVortrag.pdf",
+ paper = "Koep14.pdf",
+ video1 = "https://vimeo.com/85573338",
+ video2 = "https://vimeo.com/85573712",
+ website = "http://www.caop.org"
+}
+
+\end{chunk}
+
+\index{Daly, Timothy}
+\begin{chunk}{axiom.bib}
+@misc{Daly08,
+ author = "Daly, Timothy",
+ title = "Axiom Computer Algebra System Information Sources",
+ video = "https://www.youtube.com/watch?v=CV8y3UrpadY",
keywords = "axiomref",
 abstract =
 "Threecenter nuclear attraction and fourcenter twoelectron
 Coulomb integrals over Slatertype orbitals are required for $ab$
 initio and density functional theory molecular structure
 calculations. They occur in many millions of terms, even for small
 molecules and require rapid and accurate evaluation. The $B$
 functions are used as a basis set of atomic orbitals. These
 functions are well adapted to the Fourier transform method that
 allowed analytical expressions for the integrals of interest to be
 developed. Rapid and accurate evaluation of these analytical
 expressions is now made possible by applying the $HD$ and
 $H\overline{D}$ methods for accelerating the convergence of the
 semiinfinite oscillatory integrals. The convergence properties of
 the new methods are analyzed. The numerical results section shows
 the high predetermined accuracy and the substantial gain in the
 calculation times obtained using the new methods."
+ year = "2008"
}
\end{chunk}
\index{Adams, A.A.}
\index{Gottliebsen, H.}
\index{Linton, S.A.}
\index{Martin, U.}
+\index{Koepf, Wolfram}
\begin{chunk}{axiom.bib}
@InProceedings{Adam99a,
 author = "Adams, A.A. and Gottliebsen, H. and Linton, S.A. and Martin, U.",
 title = "VSDITLU: A verifiable symbolic definite integral table lookup",
 booktitle = "Automated Deduction",
 series = "CADE 16",
+@article{Koep99a,
+ author = "Koepf, Wolfram",
+ title = "Software for the algorithmic work with orthogonal polynomials
+ and special functions",
+ journal = "Electron. Trans. Numer. Anal.",
+ volume = "9",
year = "1999",
 location = "Trento, Italy",
 pages = "112126",
keywords = "axiomref",
 paper = "Adam99a.pdf",
 url = "http://www.acubed.info/Publications/CADE99.pdf",
+ paper = "Koep99a.pdf",
+ url = "http://arxiv.org/pdf/math/9809125v1.pdf",
abstract =
 "We present a verifiable symbolic definite integral table lookup: a
 system which matches a query, comprising a definite integral with
 parameters and side conditions, against an entry in a verifiable table
 and uses a call to a library of facts about the reals in the theorem
 prover PVS to aid in the transformation of the table entry into an
 answer. Our system is able to obtain correct answers in cases where
 standard techniques implemented in computer algebra systems fail. We
 present the full model of such a system as well as a description of
 our prototype implementation showing the efficacy of such a system:
 for example, the prototype is able to obtain correct answers in cases
 where computer algebra systems do not. We extend upon Fatemanâ€™s
 webbased table by including parametric limits of integration and
 queries with side conditions."
+ "An overview of the MAPLE routines that can be used for hypergeometric
+ and basic hypergeometric series with some discussion of how and why
+ they work."
}
\end{chunk}
\index{Aitken, William E.}
\index{Constable, Robert L.}
\index{Underwood, Judith L.}
+\index{Martin, Ursula}
\begin{chunk}{axiom.bib}
@article{Aitk99,
 author = "Aitken, William E. and Constable, Robert L. and
 Underwood, Judith L.",
 title = "Metalogical frameworks. II: Developing a reflected decision
 procedure",
 journal = "J. Autom. Reasoning",
 volume = "22",
 number = "2",
 pages = "171221",
+@InProceedings{Mart99,
+ author = "Martin, Ursula",
+ title = "Computers, reasoning and mathematical practice",
+ booktitle = "Computational Logic",
+ publisher = "Springer",
year = "1999",
+ location = "Marktoberdorf, Germany",
+ pages = "301346",
keywords = "axiomref",
 paper = "Aitk99.pdf",
 url = "http://www.nuprl.org/documents/Constable/MetalogicalFrameworksII.pdf",
 abstract =
 "Proving theorems is a creative act demanding new combinations of ideas
 and on occasion new methods of argument. For this reason, theorem
 proving systems need to be extensible. The provers should also remain
 correct under extension, so there must be a secure mechanism for doing
 this. The tacticstyle provers pioneered by Edinburgh LCF provide a
 very effective way to achieve secure extensions, but in such systems,
 all new methods must be reduced to tactics. This is a drawback because
 there are other useful proof generating tools such as decision
 procedures; these include, for example, algorithms which reduce a
 deduction problem, such as arithmetic provability, to a computation on
 graphs.

 The Nuprl system pioneered the combination of fixed decision
 procedures with tactics, but the issue of securely adding new ones was
 not solved. In this paper, we show how to safely include userdefined
 decision procedures in theorem provers. The idea is to prove
 properties of the procedure inside the proverâ€™s logic and then invoke
 a reflection rule to connect the procedure to the system. We also show
 that using a rich underlying logic permits an abstract account of the
 approach so that the results carry over to different implementations
 and other logics."
+ paper = "Mart99.pdf",
+ url =
+"http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.2061&rep=rep1&type=pdf",
+ abstract =
+ "We identify three main objectives for computer aided reasoning
+ enhancing the techniques available for mathematical experimentation,
+ developing community standards for experiment and modelling and
+ developing methods which will make computation more acceptable as part
+ of a proof. We discuss three areas of research which address these:
+ the use of theorem proving techniques to enhance or extend
+ mathematical software systems, support for formal methods techniques
+ to increase the reliability of such systems, and the use of computer
+ aided formal reasoning in support of mathematical practice. This last
+ includes activities such as formalizing systems for computational
+ mathematics or visualization so that they can still be used informally
+ but generate a formal development, and developing techniques to
+ provide assistance in the initial stages of developing a new theory.
+
+ By mathematics here we mean the activities of working research
+ mathematicians, producing new results in pure or applied mathematics,
+ although we touch briefly on some questions concerning the
+ applications of computational mathematics and simulation in research
+ science and engineering. We have left out several other related areas
+ entirely: logical questions of decidability, soundness or
+ completeness, theoretical computer science issues of semantics,
+ computability or complexity, foundational issues such as
+ constructivity, computer aided proofs about software and hardware, and
+ the use of computers in mathematical education at all levels and in
+ heuristic discovery. In particular foundational questions about
+ computation have transformed mathematical logic, computation has made
+ constructive proof feasible, and effective notions of practice for
+ proofs about hardware and software are by no means well understood.
+ However these matters fall outside the scope of this paper."
}
\end{chunk}
\index{Boulm\'e, S.}
\index{Hardin, T.}
\index{Hirschkoff, D.}
\index{Rioboo, Renaud}
\index{M\'enissierMorain, V.}
+\index{Brown, Ronald}
+\index{Tonks, Andrew}
\begin{chunk}{axiom.bib}
@InProceedings{Boul99,
 author = "Boulme, S. and Hardin, T. and Hirschkoff, D. and Rioboo, Renaud",
 title = "On the way to certify Computer Algebra Systems",
 booktitle = "Systems for integrated computation and deduction",
 series = "Calculemus 99",
 year = "1999",
 publisher = "Elsevier",
 location = "Trento, Italy",
 pages = "1112",
+@article{Brow94,
+ author = "Brown, Ronald and Tonks, Andrew",
+ title = "Calculations with simplicial and cubical groups in AXIOM",
+ journal = "Journal of Symbolic Computation",
+ volume = "17",
+ number = "2",
+ pages = "159179",
+ year = "1994",
+ month = "February",
+ misc = "CODEN JSYCEH ISSN 07477171",
keywords = "axiomref",
 paper = "Boul99.pdf",
 abstract = "
 The FOC project aims at supporting, within a coherent software system,
 the entire process of mathematical computation, starting with proved
 theories, ending with certified implementations of algorithms. In this
 paper, we explain our design requirements for the implementation,
 using polynomials as a running example. Indeed, proving correctness of
 implementations depends heavily on the way this design allows
 mathematical properties to be truly handled at the programming level.

 The FOC project, started at the fall of 1997, is aimed to build a
 programming environment for the development of certified symbolic
 computation. The working languages are Coq and Ocaml. In this paper,
 we present first the motivations of the project. We then explain why
 and how our concern for proving properties of programs has led us to
 certain implementation choices in Ocaml. This way, the sources express
 exactly the mathematical dependencies between different structures.
 This may ease the achievement of proofs."
+ paper = "Brow94.pdf",
+ abstract =
+ "Work on calculations with simplical and cubical groups in AXIOM was
+ carried out using loan equipment and software from IBM UK and guidance
+ from L. A. Lambe. We report on the results of this work, and present
+ the AXIOM code written by the second author during this period. This
+ includes an implementation of the monoids which model cubes and
+ simplices, together with a new AXIOM category of nearrings with which
+ to carry out nonabelian calculations. Examples of the use of this
+ code in interactive AXIOM sessions are also given."
}
\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 9c4efa0..7022942 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5416,6 +5416,8 @@ books/bookvolbib Axiom Citations in the Literature
buglist: add todo 339: missing side conditions
20160627.02.tpd.patch
books/bookvolbib Axiom Citations in the Literature
+20160627.03.tpd.patch
+books/bookvolbib Axiom Citations in the Literature

1.7.5.4